Natural Deduction

Deductions and logic in general are possible because this Universe has its laws. Chains of valid deductions are traced back to The First Principles and the Laws of Universe, while each step asserts the Truth of a conclusion from Truth of its premises.

All logic is domain-specific (there is no Absolute Truth), while every domain is bound by the this Universe, by what is.

The single step of a deduction, which is called syllogism, is completely general (universal) and is independent of the content of the premises and conclusion. Validity of premises is derived from a particular domain knowledge - previously established assertions (truths), traced back to the laws.

Truth (Ultimate Reality - what is) is one. Each effect has only one true (actual) non-empty set of causes - secondary effects of The Laws of the Universe, consequences of what is. Every other set is wrong - there is an infinite many of wrong explanations, invalid models, flawed chains of reasoning.

This notion of generality of a syllogism is related to programming with generic procedures, which know nothing about the data (are orthogonal to the data). CONS CAR and CDR are the classic examples - their domain is a particular structure, not the datums.


Socrates is a Man. All men are mortal. Therefore Socrates is mortal.

Notice, that the validity of this deduction is based on a categorical thinking (classification) while the categories are grounded in reality, so to speak - validated by tracing the chain of assertions back to the first principles, to what is. There are Human species, and due to the Nature of the Universe nothing is permanent - more precisely - all compound structures are impermanent. All life is nothing but a set of processes within compound atomic structures. Since life is bound by a particular atomic structures and all structures are bound by the Universe which produced the atoms, all structures are impermanent due to the laws of Nature, the law of increasing entropy in particular.

Modus Ponens

from the premise B implies A (B -> A), and from the premise B (B is True) the conclusion A (A is True) follows.

in pseudocode


Which is better stated as when B is given and a function from B to A is applied, A follows.

((lambda (x) (* 2 x)) 2)

Propositional Logic Calculus

There are 3 other axioms which are used in the Propositional Calculus.

Every known (asserted) proposition implies itself.

|- A -> A

This corresponds to the famous identity function and to the notion that primitive values are evaluating to itself (self-evaluated).

(lambda x x)

The next axiom is about discarding irrelevant facts. It reads "if you know A and that B implies A, A is known by itself". B -> A is irrelevant.

|- A -> (B -> A)

This roughly corresponds to discarding of the second argument

(lambda (x) (lambda (y) x))

The better way to express the same axiom is in terms of the logical AND (A ^ B) -> A which means A and B implies A, B is irrelevant.

The last axiom is the formalized general notion of a relationship between parts and the whole.

|- (A -> (B -> C)) -> ((A -> B) -> (A -> C))

If It is true that A implies that B implies C then it is true that A implies B implies that A implies C.

This is basically the same assertion x * (y + z) = x * y + x * z - What affects the whole affects all the parts.

From these axioms and the Modus Ponens every propositional truth could be derived.

Predicate logic

This formalizes the intuitive (but correct) notion that everything which is not true is false (Truth is unique, falsehoods are infinite).

data Bool = True | False

not True = False

Each valid step (transition) is from truth to truth only (a unique path).

(&&) True True = True

A path (deduction) is validated by recursively validating of each step up to a base-case of what is known to be the Law of Universe or its direct consequence.

foldr (&&) True

This is enough.


This stands for the fundamental rule of reduction of logic combinators (&&) and (||) - when the base case is reached the other propositions or expressions need not to be known or evaluated.

This corresponds to the notion of stopping short once I know something for sure (true or false), without examining the rest of the chain of reasoning.

false && e --> false
true || e --> true

This process stops once a True is found

any p = foldr (\x xs -> p x || xs) False

This process stops once a False is found

all p = foldr (\x xs -> p x && xs) True

Such that

The notion of such that - a subset which satisfies a given predicate is captured in a filter function or could be expresses in a comprehension with a guard

(item for item in iterable if function(item))
[x | x <- xs, p x]
Last modified 2 years ago Last modified on Dec 3, 2017, 11:20:37 AM
Note: See TracWiki for help on using the wiki.