1. Fundamental assumptions

In some ways, logic is fundamental to everything else, but this does not mean that logic can be stated without prior assumptions.

Here, unlike normal treatments

• logic is taken as a specific extension of natural language

that arises when three things are done:

• The natural language is extended with variables;

• it is declared which expressions are part of logic; and

• some rules of inference are assumed for the logical expressions

Thus one starts with assuming that one has some natural language - like English, in the present case - one knows fairly well, including its basic logical terms and their common usages, and then attempts to state rules for logical inference by adding variables to the natural language and by defining what count as the well-formed and meaningful expressions of the extended language.

And another fundamental assumption is that, e.g. from natural language, one knows and is familiar with the concept of a sequence, and in particular a sequence of terms, such as make up a statement in natural language. The terms in a sequence of terms are separated from each other by spaces or commas, and are themselves sequences of letters without the comma or the space.

2. Symbols

Variables for things: undercast letters with or without numerical suffix
Variables for statements: uppercast letters with or without numerical suffix
Variables for structures: uppercast letters with or without numerical suffix 

A variable is a term that differs from all non-variables and may be replaced conditionally by other variables of the same kind, or constants of the kind. The kind of a variable depends on what sort of term it may be replaced with: Terms for things or classes of things, which are name-like or noun-like in English; terms for possible facts, which are statements; or terms for what remains of a statement when one disregards one or more of its variables, for which we use the term structures, that covers predicates and relations. 

Interpunction

Logical constants

Logical constants: '|-' '|=' '&' 'V' '~' '..' '|' '='

There are special symbols to be introduced, next to the variables, that are used for logical constants. Their readings are as follows, with the meanings associated to them by trained speakers of English, but to be rendered more precise by the rules that follow.

'T₁ .. T_n'         for 'a sequence of T₁ .. T_n'
'|- S'              for 'One may write that S'
'S₁ .. S_n |= T'  for 'If one may write that S₁ .. S_n, then one may write that T'
'S₁&S₂'           for 'S₁ and S₂'
'S₁VS₂'           for 'S₁ or S₂'
'~S₁'              for 'not S₁'
'S_a|S_b.S'         for 'S with S_a uniformally substituted for S_b in S'
'S₁ --> S₂'       for 'S₁ implies S₂'
'S₁ IFF S₂'       for 'S₁ if and only if S₂'

As just pointed out, the symbolical expressions on the left are made more precise by the rules that follow, but are to be taken as having a meaning that is adequately rendered on the right.

The notation for sequences presupposes that one supplies what is missing on the dots, wherever necessary, from the suggestion made by the suffices. Thus 'T₁ .. T₄' is short for 'T₁ T₂ T₃ T₄' and 'S_f .. S_j' is short for 'S_f S_g S_h S_i S_j'.

Grammar of propositional logic

To obtain a logic for statements or propositions, we need to specify what counts as a proposition. Here is a convenient set of principles that says how to obtain more complex propositions from more simple ones, namely by introducing logical constants:

G1. If (P) is a proposition, (~(P)) is a proposition.
G2. If (P) and (Q) are propositions, (P&Q) and (PVQ) are propositions.
G3. Nothing else is a proposition unless by explicit definition.

Here it is not laid down what are propositions, but only how to obtain propositions with logical constants from given propositions.

Substitution rules

To formulate rules for substitution it is convenient to introduce some definitions. First, the term 'expression' stands for 'a sequence of terms', regardless of whether we can attribute a meaning to an expression.

Next, if A and B are two expressions, then B is said to be a variant of A if and only if whenever the i-th and the j-th terms of A are the same so are the i-th and the j-th terms of B and whenever the i-th term of A is a constant the i-th term of B is the same constant.

Intuitively speaking, a variant of A is just the same as A except for variables, and the variables of a variant of A preserve the pattern of the variables in A.

|- If |-S and if S' is a variant of S, then |-S'

This is the basic rule of substitution. To be valid it must have the property that in any case that S is true, then S' is also true, and that depends on the rules that allow one to make substitutions according to the above general rule.

There is also need for another rule, since variants are always of the same length:

|- If |-S_a then |-S_b|S_c.S_a if S_b does not contain any variable contained in S_a.

This says that if S_a may be written so may be the result of any uniform substitution in S_a. It enables the inference of e.g. (S_x&S_y)V~(S_x&S_y) from (S_zV~S_z) substituting S_x&S_y for S_z.

Below there will be a more refined treatment of substitution when variables for terms and structures are also considered.

Argument rules

|- (S_i |= S_i)
|- (S_k |= S_n  |= ~S_k V S_n)
|- (~S_k V S_n |=  S_k |= S_n)

These rules insist that one may always write that a statement can be inferred from itself, and gives ways to restate what inferring from amounts to in terms of other logical constants, namely not and or.

Any statement of the form '|- (A1 .. An |= C)' is called an inference rule, and each of the A1 .. An a premiss, with C the conclusion.

Assumption rules

|- (S_i*)
|- (S S_i* .. S_n) |= (S S_i |= S_n)) - if S_i is the last assumption in (S S_i* .. S_n)

The first rule says one always may make an assumption, and the star indicates that in fact S_i is inferred by the rule that one may assume what one pleases, and is an assumption. This is called the rule of assumption introduction.

The second rule states and shows how to get rid of assumptions in a sequence of inferences: If S_i is the last assumption in the sequence, all conclusions after it are entailed by it (and what preceeds it, indicated by S). This is called the rule of assumption elimination.

Conjunction rules

|- (S_i .. S_k) |= (S_i&S_k)
|- (S_i&S_k)   |= (S_i)
|- (S_i&S_k)   |= (S_k)

The rules for 'and' as used between statements: If one has already inferred both Si and Sk one may also infer their conjunction, and if one has inferred a conjunction, one may infer each of the conjuncts.

Disjunction rules

|- (S_i)                  |= (S_iVS_j)
|- (S_j)                  |= (S_iVS_j)
|- (S_iVS_j .. ~S_iVS_j) |= (S_j)

The rules for 'or' as used between statements: If one has inferred a statement, one can infer it as part of a disjunction with an arbitrary statement, and if one has inferred two disjunctions of the forms S_iVS_j and ~S_iVS_j then one may infer S_j directly.

Definitions of logical constants

|- 'S_i --> S_j' for '~S_iVS_j'
|- 'S_i IFF S_j' for 'S_i --> S_j & S_j --> S_i'

The above rules are sufficient to derive the standard systems of propositional logic in terms of proof theory, i.e. the standard theorems of classical propositional logic can be proved from the above rules. (See: MT 2.)

Structures

Logical constants: '=' '≠' 'Z[t₁ .. t_n]' ' 'x|y:' '|x.' '(Ex)' '(x)' '#'

The above related to the logic of statements. Here we have arrived at the logic of terms and structures, which needs more terminology, that is listed above and explained below.

Readings of logical constants

'a=b'                        for 'a equals b'
'a≠b'                        for 'a does not equal b'
'Z[t₁ .. t_n]'               for 'Z relates t₁ .. t_n' or 'Z t₁ .. t_n'
'x|y.Z[t₁ .. y .. t_n]'    for 'x substitutes for y in Z[t₁ .. y .. t_n]'
'|x:Z[y₁ .. x .. y_n]'     for 'the x such that Z[y₁ .. x .. y_n]'
'Ø'                           for '|x.(x≠x)'         
'(Ex).S[y₁ .. x .. y_n]'   for 'there is an x such that S[y₁ .. x .. y_n]'
'(x).S[y₁ .. x .. y_n]'     for 'every x is such that S[y₁ .. x .. y_n]'
'#(Y)'                       for 'the number of Y'

The signs and readings for equality and inequality are standard.

The point of the notation 'Z[t₁ .. t_n]' that obtains a structure-term from a statement by replacing some constant(s) by some variable(s) in the statement: The structure-term is the statement apart from the variable(s), and indeed it makes sense to say that the structure-term relates the other terms in a statement. An alternative name for the notation is formula: A statement with one or more variables as terms, or obtained from such a statement by substitution for the variables.

The point of 'x|y.Z[t₁ .. y .. t_n]' is to have an explicit symbolism for substitutions and replacements of terms in structure-terms or formulas.

The notation '|x:S[y₁ .. x .. y_n]' codifies the idea of abstraction, and does so by using formulas and a prefix that is used in binary form for substitutions.

The term 'Ø' is a standard mathematical symbol for 'nothing', and is here defined using abstraction and identity: The term nothing represents the same as what the things that are not equal to themselves represent.

The terms '(Ex).S[y₁ .. x .. y_n]' and '(x).S[y₁ .. x .. y_n]' are the standard quantifiers 'for some x' and 'for every x', in the above rendered as prefixes of formulas in which 'x' occurs somewhere.

Finally, the notation '#(Y)' is used to abbreviate the phrase 'the number of Y' and is written using standard functional notation.

Grammar of predicate logic

G1. If P is an n-place predicate and s1 .. sn are n subjects, P(s1 .. sn) is a proposition.
G2. If P(s1 .. sn) is a proposition and one or more of s1 .. sn is replaced by a subject variable, the result is a formula. 
G3. Formulas are propositions.
G4. If Z is a formula and v1 .. vn are subject-variables, then |v1 .. vn: Z is a subject-term.
G5. If s1 and s2 are subject-terms, s1=s2 is a formula.

Structural rule

|- (t₁)..(t_n)(v₁)..(v_k)(ET)((t₁ .. v₁ .. t_i .. v_k .. t_n)=T[v₁ .. v_k])

Here in fact the notion of sequence of terms is used to claim that every sequence of terms that contains some variables can be identified with a structure-term followed by the variables.

Linguistically speaking, this amounts to the assumption that one can introduce some convenient abbreviation for any long formula.

Substitution rules for equalities

|- ('A' for 'B'                                   IFF A=B)

This rule takes care of quite a number of occurences of the phrase 'for' in the above, for it restates these in terms of equalities, that are governed by the following rules: 

|- ( T[..x..] & x=y                            IFF T[..y..] & x=y )
|- ( a|b.c = c                                  IFF b≠c )
|- ( a|b.c = a                                  IFF b=c )

The first rule lays down what an equality amounts to for a term in a formula, and the other two rules govern equalities for substitutions of terms for terms. All three of these rules are used together with the threesome that follows.

Substitution rules and variants

Variants were mentioned above, and can be defined here using 'CON' for 'Constant', which includes logical terms:

|- (b₁ .. b_n) e var(a₁ .. a_n) IFF (i)(a_i e CON --> b_i=a_i) & (i)(j)(a_i=a_j IFF b_i=b_j)

A sequence of terms B is a variant of a sequence of terms A precisely if whenever the i-th term of B is a constant the i-th term of A is a constant and whenever the i-th and the j-th terms of A are the same so are the i-th and the j-th terms of B.

The general rule of substitution of variants now can be stated thus:

|- { ((A') e var(A)) & (A)} |= (A')

In words: A variant of a theorem is a theorem. It is in fact this rule that gives variables a general interpretation and that allows reasoning by substitutions in established formulas.

It may also be noted that the definition of variant implies that where y is a variable and y|x.T[x] holds, and c is a constant, c|x.T[x] is a variant of y|x.T[x]. Thus, if some formula holds for every substitution, it holds also for every constant.

Substitution rules for terms

|- ( x|y.(t₁ .. t_n)                           IFF (x|y.t₁ .. x|y.t_n) )
|- ( (x₁ .. x_n)|(y₁ .. y_n).(t₁ .. t_n)      IFF x₁|y₁ .. x_n|y_n.(t₁ .. t_n) )
|- ( x₁|y₁ x₂|y₂ .. x_n|y_n.(t₁ .. t_n)     IFF x₂|y₂ .. x_n|y_n.(x₁|y₁.t₁ .. x₁|y₁.t_n) )

The first of these states what a substitution of a term in a sequence amounts to: A sequence where each term gets substituted when appropriate (as governed by the rules in the previous group).

The second is a convenience that allows one to switch between a shorter and a longer formulation for sequences of substitutions.

The third governs how a sequence of substitutions for a formula is to be done: The leftmost substitution is first made in the formula (and skips the other substituends).

Substitution rules for statements and structures

|- ( S_j |= S_k                                 IFF a|b.S_j |= a|b.S_k)
|- ( a|b.S[..b..]                            IFF S[..b..] |= S[..a..] )

The first of these states for terms what was earlier stated for statements, and the second shows and states what is involved in valid substitutions in truths: one moves from truth to truth.

Abstractions and elements

|- ( |x:S[x] = |x:T[x]                      IFF y|x. S[x] IFF T[x] )
|- ( (a₁ .. a_n) e |x₁ .. x_n. S[x₁ .. x_n]  IFF a₁|x₁ .. a_n|x_n. S[x₁ .. x_n] )

The first effectively explains abstraction in terms of equality and substitutions in formulas: Two abstracts are equal precisely if the equivalence of their formulas is true under arbitrary substitutions (of the proper kinds of terms).

It is well to notice here that y|x. S[x] IFF T[x] is general given the rule of substitution: If one can prove this, where y is a variable, one therefore can prove z|x. S[x] IFF T[x] or any other alphabetical variant of variables.

The second explains elementhood in terms of abstraction. Here it is restated for the case n=1: a₁ is an element of the x₁ that are S[x₁] precisely if a₁ can be validly substituted for x₁ in S[x₁] i.e. if and only if S[a₁].

Quantified structures

|- ( (x).S(..x..)                             IFF |x: ~S(..x..) = Ø )
|- ( (x).~S(..x..)                           IFF |x: S(..x..) = Ø )
|- ( (Ex).S(..x..)                            IFF |x: S(..x..) ≠ Ø )
|- ( (Ex).~S(..x..)                          IFF |x: ~S(..x..) ≠ Ø )

The standard quantifiers - for every and for some - get in effect rendered by equalities or inequalities of structures with nothing: Every thing is S precisely if the things that are not S equals nothing; every thing is not S precisely if the things that are S equals nothing; some thing is S precisely if the things that are S does not equal nothing, and some thing is not S precisely if the things that are not S does not equal nothing.

Structures, functions and mappings

|- Structure[Z X₁ .. X_n] IFF (y₁)..(y_n)((y₁ .. y_n) e |x₁..x_n.Z[x₁..x_n] IFF
                                                   y₁eX₁ & .. & y_neX_n & Z[y₁..y_n])
|- Function[F X₁ .. Xn]  IFF Structure[F X₁ .. X_n] &
                                      (y₁)..(y_m)(y_n)(y_x)( ((y₁..y_m y_n) e F  &
                                                                 (y₁..y_m y_x) e F)  |= y_n=y_x)
|- Mapping[F X₁ X₂]      IFF Function[F X₁ X₂] & Function[F X₂ X₁]
|- #(S_i)=#(S_j)              IFF (EF)(Mapping[F S_i S_j])
|- F(x₁ .. x_n)=y            IFF (EX₁) .. (EX_m)(EX_n)(Function[F X₁ .. X_m X_n] &
                                                                 (x₁ .. x_m y) e F).

This concerns the tools and assumptions for the basics of mathematics.

A Structure made up of Z and X₁ .. X_n is in effect the sequences of things that satisfy a formula while being of appropriate kinds X₁ .. X_n. A Function is a structure-term with a special property: Its last term is unique in any case. And a Mapping is a binary function between X₁ and X₂ that holds both ways. And the number of S_i equals the number of S_j precisely if there is a mapping between S_i and S_j. The last assumption is a convenience that explains the standard functional notation F(x₁ .. x_n)=y.

Arguments

An argument in BL is a sequence of numbered statements with the property that each statement in it is inferred by assumption introduction or is the consequence in a variant of an assumed or proved inference rule of which the premisses occur before the consequence in the argument or is an instance of an already proved formula.

Note this implies every argument must start from assumptions. Also note that this does not imply, without further assumption, that what is correctly proved by the above criterion also is validly proved - though this does follow if one has proved that all rules of inference are valid i.e. have the property that their consequences cannot fail to be true if their premisses are all true.

And a further point to notice is that, given a sequence of statements in which the assumptions are marked, and a sequence of rules of inference, one can mechanically decide by the above criterion whether or not the sequence of statements is a correct argument.

This is important, because this is the basis for one's trust in and reliance on logical argument: One can prove that a purported argument is or is not a correct argument given a series of rules of inference, and one can prove that a purported argument is valid given a series of rules of inference by proving that it is correct and all the rules of inference that were used in the argument are valid.

Two reasons why this is important are the following.

First, it gives a clear idea of what a proof would be, and indeed a way of checking any purported proof mechanically for correctness.

Second, it shifts all problems of deductive inference back to whatever rules of inference were assumed: If only these are valid, then everything that is proved using these rules must be valid too.