= 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.
== Syllogism ==
{{{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
{{{
WHEN (B -> A) AND B
A
}}}
Which is better stated as ''when B is given and a function from B to A is applied, A follows''.
{{{#!scheme
((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).
{{{#!scheme
(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
{{{#!scheme
(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).
{{{#!haskell
data Bool = True | False
not True = False
}}}
Each valid step (transition) is from truth to truth only (a unique path).
{{{#!haskell
(&&) 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.
{{{#!haskell
foldr (&&) True
}}}
This is enough.
== Short-circuiting ==
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.
{{{#!scala
false && e --> false
true || e --> true
}}}
This process stops once a {{{True}}} is found
{{{#!haskell
any p = foldr (\x xs -> p x || xs) False
}}}
This process stops once a {{{False}}} is found
{{{#!haskell
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 [wiki:/Functions/Filter filter] function or could be expresses in a
''comprehension'' with a ''guard''
{{{#!python
(item for item in iterable if function(item))
}}}
{{{#!haskell
[x | x <- xs, p x]
}}}