8/1/26
The program, widgets, or Notes, should be accompanied by a suitable textbook, such as:
M.Bergmann, J.Moor, J.Nelson, The Logic Book
A.Hausman, H.Kahane, P.Tidman, Logic and Philosophy
W.Hodges, Logic
C.Howson, Logic with Trees
R.C.Jeffrey, Formal Logic: Its Scope and Limits
H.Leblanc and W.Wisdom, Deductive Logic
B.Mates, Elementary Logic
M.D.Resnick, Elementary Logic
Unfortunately these textbooks use slightly different choices of rules and symbols one from another. To adjust to this the Notes are in different major sections, with the sections tailored to particular texts.
You are invited to review
Notation
Not all logicians, and logical texts, use the same symbols for the so-called 'logical connectives'. Nor do they use the same sequences of symbols for 'well formed formulas'.
Here are typical possibilities for symbols
'not' : ∼ (the 'tilde'), ¬ (looks like the top right corner of a box)
'and': ∧, & (the ampersand), . (just a period)
'or': ∨ (usually just this, vel)
'implication': ⊃ , →
'equivalence': ≡, ↔
'existential quantifier': ∃, ∑
'universal quantifier':∀, ∏
So, in a logic book, you might see (A&B)→C and that is just the same as (A∧B)⊃C.
And you might see (∀x)(Fx ⊃ Gxy) and that might be just the same as ∀x(F(x)→G(x,y)).
The software running here can easily manage or render any of these. But we should explain what we favor, and help you find what you prefer.
The 'gentzen' system
This uses Rabc for the application of a predicate R to the arguments or terms a, b, c, and the use of f(abc) for the application of a functor or function f to the arguments a, b, c. i.e the predicates and atomic terms are of length 1. It uses the upper case letters A-Z to be predicates, so, for example, R, S, T are all predicates. And it employs lower case letters ie [a--v], perhaps followed by subscripts, to be constant terms or functions. Variables, consist of lower case [w-z]. There are parentheses around the quantifiers. The gentzen system also uses ~, ∧, v, ⊃, ≡, so a typical formula is (∀x)(Fx∧~Hx ⊃ Gxy).
Formation Rules for the Gentzen System
Terms, constants, variables, propositions, and predicates
Terms
<constant> ::= (['0'-'9']) |'∅'| 'U'|'{ }'
<subscript> ::= ['₁'-'₉']
<functor> ::= ['a'-'v'](< subscript >)*
<variable> ::= ['w'-'z'](< subscript >)*
<term> ::=<constant>|
<functor>|
<variable>|
<functor>((<term>)+)|
<functor>((<term>)+ (,<term>)*)+|
{((<term>)+ (,<term>)*)+}|
(<term>)|
℘ (<term>)|
<term>(''')+|
<term>+<term>|
<term>-<term>|
<term>.<term>|
<term>∪<term>|
<term>∩<term>|
<<term>,<term>>|
{<variable>:<wff>}
{<variable>|<wff>}
For example, 5, ∅, a, w, b₁₂, z₁₂₁₂, f(abc), f(a,b,c), {a,b,c}, (5), ℘(x), 5''' , 1+2, 2-3, x.2, a∪b, x∩y, <a,b>, {x:Px}, {x|Px&Qy} are all terms.
(Atomic) constants
<atomicConstant> ::= <constant>|<functor>
That is 'a' through 'v' , possibly with subscripts, and the numerals and some set theory constants.
Variables
'w' through 'z' , possibly with subscripts.
Types
'a' through 'v' , possibly with subscripts.
Propositions and Predicates
<predicator> ::= ['A'-'Z'](< subscript >)*
<proposition> ::=<predicator>(< term >)*|
⊤|
⊥|
The predicate letters are upper case A-Z, possibly with subscripts. Then propositions are these followed by zero or more terms, for example, P, Q₁₂f(abc), or X12 . There is also 'top' ⊤ and 'bottom' ⊥ which are pre-defined propositions for true and false.
Well Formed Formulas (WFFs)
<wff> ::=
<proposition>|
<term1> = <term2>|
<term1> < <term2>|
<term1> > <term2>|
<term1> ε <term2>|
(<wff>)|
∼<wff>|
<wff1> ∧<wff2>|
<wff1> ∨<wff2>|
<wff1> ⊃ <wff2>
<wff1> ≡<wff2>|
(∀<variable>) <wff>|
∀<variable> <wff>|
(∃<variable>) <wff>|
(∃<variable>!) <wff>|
|∀<variable>:<type>) <wff>|
(∃<variable>:<type>) <wff>|
□<wff>|
◊<wff>|
Κ<term> <wff>|
Ρ<term> <wff>|
For example, P, Pa, Qbv, (∀x)Hxy are all well-formed formulas and so too are a=b and (∃x)(x=d).
Brackets are used to clarify or disambiguate expressions.