🏗️ ΘρϵηΠατπ🚧 (under construction)

True and False
True and false denoted by T,F respectively are distinct symbols ( TF ).
Predicate
A predicate is a function f:X{T,F} for some set X
Logical And
We define the function :{T,F}×{T,F}{T,F} by the following table: TTTTFFFTFFFF note that we use infix notation for this function.
Logical Negation
We define the function ¬:{T,F}{T,F} by the following table: p¬pTFFT

When working with the negation, we almost never include the parenthesis unless it is really necessary, so you'll see ¬T=F rather than the standard function notation: ¬(T)=F

Logical Or
We define :{T,F}×{T,F}{T,F} as pq:=¬(¬p¬q)
Rightward Logical Implication
We define :{T,F}×{T,F}{T,F} as pq:=¬pq

Note that even though the above doesn't seem intuitive, it exactly matches your intuition, we know that the only time an implication can be false is when we have the antecdent to be true, but the result false, which is exactly the case for the above definition.

Usually p is called the "antecedent" and q the "consequent".

Leftward Logical Implication
We define :{T,F}×{T,F}{T,F} as pq:=qp
Logical Bi-Implication
We define :{T,F}×{T,F}{T,F} as pq:=(pq)(pq)

Note that in writing mathematicians will use the word "iff" as short-hand for if and only if, which represents the bi-implication.

Logical And True iff both Arguments are True
pq=Tp=Tq=T

The above proof might feel a bit meta, indeed, we are using the definition of "iff" that we just defined on this page. The "metaness" is coming from the fact that the "iff" we use in english language is actually the bi-implication which we formally define a bit later in the page (which in-turn is then defined in terms of logical and eventually).

Logical Exclusive Or
We define :{T,F}×{T,F}{T,F} as pq:=(¬pq)(p¬q)

"XOR" is sometimes used in place of it's regular name.

Addition Mod 2 is Associative
Suppose that we have the function p:{0,1}{0,1} defined such that
  • p(0,0)=p(1,1)=0
  • p(0,1)=p(1,0)=1
then it is associative
Exclusive Or is Associative
For any x1,x2,x3{T,F} we have that (x1x2)x3=x1(x2x3)
Sum of Ones Mod 2 becomes 0 iff Even
Since p is associative let's use it as a binary operation and temporarily label it as + then consider a sequence (an):N0{0,1} i=0kan=0 if and only if |{aj:aj=1}| is even.
Exclusive Or Evaluates to True iff an odd number of arguments are True
x1x2xk=T if and only if i=1kxi is odd.
Tautology
We say that a predicate P:X{T,F} is a tautology iff for every xA,P(x)=T.

In mathematics, when we prove a statement, we are actually showing that it is a tautology.

Contrapositive
The following is a tautology (pq)(¬q¬p)
Forced Consequence
The following is a tautology (Tp)p=T
Arbitrary And
For any nN0 we define arbitrary and as the predicate :{T,F}n{T,F} such that for any X=(x1,,xn){T,F}n. X=T if and only if the following statement holds true i{1,,n},xi=T
Empty And is True
Suppose that X=() (the empty tuple), then X=T where we've used the the arbitrary and
Arbitrary And Indexed Notation
Suppose that, a,bZ and pa,pb{T,F} then we define i=abpi:=(pa,,pb) where we've used the the arbitrary and
Arbitrary And Indexed Notation with Reversed Integers is True
Suppose a>bZ and i=abpi=T
Arbitrary And Expanded Notation
Suppose that p1,pn{T,F} then we define p1pn:=i=1npi where we've used the previous definition
Arbitrary Or
Uniqueness
Suppose that P:X{T,F} is a predicate, then we say that there is a unique element which satisfies P over the set SX when sS,P(s)tS,P(t)t=s
For Every, There Exists is a Function
The statement xX,yY,P(x,y) is equivalent to f:XY,xX,P(x,f(x))