Today I Learned

Some of the things I've learned every day since Oct 10, 2016

Category Archives: logic

131: Pierce’s Law

In classical logic, Pierce’s Law is the property that

((P \rightarrow Q) \rightarrow P) \rightarrow P.


(P \rightarrow Q) \rightarrow P


\overline{P \rightarrow Q} \vee P


\overline{\overline{P} \vee Q} \vee P


(P \wedge \overline{Q}) \vee P


(P \wedge \overline{Q}) \vee (P \wedge 1)



130: Consequentia Mirabilis

Consequentia Mirabilis, also known as Clavius’ Law (after the German mathematician) is the principal in classical logic

(\neg X \rightarrow X) \rightarrow X.

That is, it’s the principle that if a proposition’s negation implies the proposition, then the proposition must be true.

Its use is similar in form to that reductio ad absurdum. To use reductio ad absurdum, one assumes that a proposition is false, sees that a contradiction follows, and from this concludes that the proposition must be true. To use consequentia mirabilis, by contrast, one assumes that a proposition is false, sees that the proposition itself follows, and from this concludes that the proposition must be true.

126: Principle of Explosion

In logic systems such as classical logic, the principle of explosion is the principle that from a contradiction any proposition can be inferred to be true.

To show this, suppose we’ve arrived at a contradictory statement, P \wedge \neg P. Let Q be any proposition we want to prove. By conjunction elimination, we have P, and then by disjunction introduction we have

P \vee Q.

However, since we also have \neg P, it follows that Q is true.

This principle suggests an interesting alternative attitude towards contradiction in systems that exhibit this behavior: contradiction is not undesirable because of any ‘intuitive’ nonsensicalness, but simply because a set of assumptions leading to contradiction gives us no information.

117: Generality of the 2-Element Boolean Algebra

The behavior of boolean algebras in general is captured by that of 2, the boolean algebra with 2 elements, since a theorem holds for 2 if and only if it also holds for any boolean algebra.

113: One Generalization of AND, OR, NOT to Fuzzy Logic

In fuzzy logic, where the set \{ 0, 1 \} of possible values is replaced with the range [ 0, 1], generalizations of the basic AND, OR, and NOT operators is needed which can handle input from the new domain. The only requirement of such generalizations is that they agree with their more specific counterparts when given input from \{ 0, 1 \}. However, there are choices which are more intuitive and advantageous than others.

One such choice is defining

  • AND(a, b) = a*b
  • OR(a, b) = a + b – a*b
  • NOT(a) = 1 – a

The formulas for AND and NOT are intuitive enough, and even though the formula for OR may not be, it’s easily derived from those of the other 2 using the equivalence

OR(a, b) = NOT(AND(NOT(a), NOT(b))).


69: The Deduction Theorem

In logic, the deduction theorem states that where A, B are formulas and \Delta is a set of assumptions or axioms, the implication A \rightarrow B is deducible from \Delta if and only if B is deducible from \Delta \bigcup \{A\}. The statement is intuitive, but wasn’t formally proven until 1930.

51: Undecidability of Equality of Lambda Expressions

In general, there is no algorithm which determines whether two lambda expressions are equivalent under the reduction rules of the lambda calculus. This is the problem for which the first proof of undecidability was given.

50: Normalization Property (Lambda Calculus)

In a rewrite system, such as \beta-reduction in the lambda calculus, a term may or may not satisfy either the  weak normalization or the strong normalization property.

A term T satisfies the weak normalization property if there exists a sequence of rewrites on T that eventually results in a normal form of T: a term which is irreducible.

A term T satisfies the strong normalization property if every sequence of rewrites on T eventually results in a normal form of T.

If every term in a rewrite system satisfies the [weak | strong] normalization property, then the system itself is said to satisfy the same property.


An example of a system which satisfies neither of the normalization properties is the pure untyped lambda calculus. An example of a non-normal term within this system is

(\lambda y . y y) (\lambda y . y y).

Under \beta-reduction, this term reduces to itself, and so it never terminates in an irreducible form.

Conversely, a term within this system which is weakly normal is

(\lambda x . x) x.

Under \beta-reduction, this term reduces to just the variable x, an irreducible term.

There are other forms of the lambda calculus, as well as other similar systems, which are normal. These can be viewed as programming languages in which every program eventually will (or can) terminate. A significant drawback to such a system, however, is that if a system is normal it cannot be Turing complete.

Additionally, in the lambda calculus every normalizing term has a unique normal form.

49: Church Numerals

In Church encoding, an encoding system using lambda calculus, the Church numerals are the representation of the natural numbers. The distinguishing feature of the Church numerals is that the natural numbers are not treated as a primitive type, as they would typically be, but are simply represented by higher-order functions. Each higher-order function \boldsymbol{n} representing the number n takes two arguments — a function f and a second argument to be passed to f — and returns the n-fold composition of f.


0 is represented as \boldsymbol{0} = \lambda f . \lambda x . x, which given any function f returns a function which simply returns x without applying f at all.

1 is represented as \boldsymbol{1} = \lambda f . \lambda x . f x, which given any function f returns a function which applies f once to x.

2 is represented as \boldsymbol{2} = \lambda f . \lambda x . f (f x), which given any function f returns a function which applies f twice to x.

3 is represented as \boldsymbol{3} = \lambda f . \lambda x . f (f (f x)), which given any function f returns a function which applies f three times to x.