================================================================================
UTF-8-file qedeq_logic_v1
Generated from http://www.qedeq.org/0_04_01/doc/math/qedeq_logic_v1.xml
Generated at 2011-03-04 22:48:52.913
================================================================================
If the characters of this document don't display correctly try opening this
document within a webbrowser and if necessary change the encoding to
Unicode (UTF-8)
Permission is granted to copy, distribute and/or modify this document
under the terms of the GNU Free Documentation License, Version 1.2
or any later version published by the Free Software Foundation;
with no Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts.
Elements of Mathematical Logic
══════════════════════════════
Michael Meyling
The source for this document can be found here:
http://www.qedeq.org/0_04_01/doc/math/qedeq_logic_v1.xml
Copyright by the authors. All rights reserved.
If you have any questions, suggestions or want to add something to the list of
modules that use this one, please send an email to the address mime@qedeq.org
The authors of this document are:
Michael Meyling
___________________________________________________
Summary
═══════
The project Ｈｉｌｂｅｒｔ ＩＩ deals with the formal presentation and documentation of
mathematical knowledge. For this reason Ｈｉｌｂｅｒｔ ＩＩ provides a program suite to
accomplish that tasks. The concrete documentation of mathematical basics is also
a purpose of this project. For further informations about the Ｈｉｌｂｅｒｔ ＩＩ project
see under http://www.qedeq.org .
This document describes the logical axioms and the rules and meta rules that are
used to derive new propositions.
The presentation is axiomatic and in a formal form. A formal calculus is given
that enables us to derive all true formulas. Additional derived rules, theorems,
definitions, abbreviations and syntax extensions basically correspond with the
mathematical practice.
This document is also written in a formal language, the original text is a XML
file with a syntax defined by the XSD
http://www.qedeq.org/current/xml/qedeq.xsd .
This document is work in progress and is updated from time to time. Especially
at the locations marked by „+++” additions or changes will take place.
___________________________________________________
Foreword
════════
The whole mathematical universe can be unfolded by set‒theoretic means. Beside
the set‒theoretic axioms only logical axioms and rules are required. These
elementary basics are sufficient to define the most complex mathematical
structures and enable us to prove propositions for those structures. This
approach can be fully formalized and can be reduced to simple manipulations of
character strings. The semantical interpretation of these character strings
represent the mathematical universum.
It is more than convenient to introduce abbreviations and use further derivation
rules. But these comforts could be eliminated and replaced by the basic terms at
any time
┌
│ At least this is theoretically possible. This transformation is not
│ in each case practically realizable due to restrictions in time and
│ space. For example it is not possible to write down the natural
│ number 1,000,000,000 completely in set notation.
└
.
This project has its source in a childhood dream to undertake a formalization of
mathematics. In the meantime the technical possibilities are highly developed so
that a realization seems within reach.
Special thanks go to the professors W . K e r b y and V . G ü n t h e r of
the university of Hamburg for their inspiring lectures about logic and axiomatic
set theory. Without these important impulses this project would not exist.
I am deeply grateful to my wife G e s i n e D r ä g e r and our son
L e n n a r t for their support and patience.
Hamburg, december, 2010
Michael Meyling
___________________________________________________
Introduction
════════════
At the beginning we quote D . H i l b e r t from the lecture „The Logical
Basis of Mathematics”, September 1922
┌
│ Lecture given at the Deutsche Naturforscher-Gesellschaft, September
│ 1922.
└
.
„The fundamental idea of my proof theory is the following:
All the propositions that constitute in mathematics are converted into
formulas, so that mathematics proper becomes all inventory of formulas.
These differ from the ordinary formulas of mathematics only in that,
besides the ordinary signs, the logical signs especially „implies” (→) and
for „not” (‾ ) occur in them. Certain formulas, which serve as building
blocks for the formal edifice of mathematics, are called axioms. A proof
is an array that must be given as such to our perceptual intuition of it
of inferences according to the schema
A
A → B
_______________________________________
B
where each of the premises, that is, the formulae, A and A → B in the
array either is an axiom or directly from an axiom by substitution, or
else coincides with the end formula B of an inference occurring earlier in
the proof or results from it by substitution. A formula is said to be
provable if it is either an axiom or the end formula of a proof.”
At the beginning there is logic. Logic is the analysis of methods of reasoning.
It helps to derive new propositions from already given ones. Logic is
universally applicable.
In the 1928 published book G r u n d z ü g e d e r
t h e o r e t i s c h e n L o g i k (Principles of Theoretical Logic)
D . H i l b e r t and W . A c k e r m a n n formalized propositional
calculus in a way that build the basis for the logical system used here. 1959
P . S . N o v i k o v specified a refined axiom and rule system for
predicate calculus.
In this text we present a first order predicate calculus with identity and
functors that is the starting point for the development of the mathematical
theory. Only the results without any proofs and in short form are given in the
following.
┌
│ If there is time proofs will be added.
└
___________________________________________________
Chapter 1
Language
════════
In this chapter we define a formal language to express mathematical propositions
in a very precise way. Although this document describes a very formal approach
to express mathematical content it is not sufficent to serve as a definition for
an computer readable document format. Therefore such an extensive specification
has to be done elsewhere. The choosen format is the E x t e n s i b l e
M a r k u p L a n g u a g e abbreviated X M L . XML is a set of rules for
encoding documents electronically.
┌
│ See http://www.w3.org/XML/ for more information.
└
The according formal syntax specification can be found at
http://www.qedeq.org/current/xml/qedeq.xsd . It specifies a complete
mathematical document format that enables the generation of LaTeX books and
makes automatic proof checking possible. Further syntax restrictions and some
explanations can be found at
http://www.qedeq.org/current/doc/project/qedeq_logic_language_en.pdf .
Even this document is (or was generated) from an XML file that can be found
here: http://wwww.qedeq.org/0_04_01/doc/math/qedeq_logic_v1.xml . But now we
just follow the traditional mathematical way to present the elements of
mathematical logic.
1.1 Terms and Formulas
――――――――――――――――――――――
We use the l o g i c a l s y m b o l s L = { ‘¬’, ‘∧’, ‘∨’, ‘↔’, ‘→’, ‘∀’,
∃’ }, the p r e d i c a t e c o n s t a n t s C = {c^k_i | i, k ∈ ω}, the
f u n c t i o n v a r i a b l e s
┌
│ Function variables are used for a shorter notation. For example
│ writing an identity proposition x = y → f(x) = f(y). Also this
│ introduction prepares for the syntax extension for functional
│ classes.
└
F = {f^k_i | i, k ∈ ω ∧ k > 0}, the f u n c t i o n c o n s t a n t s
┌
│ Function constants are also introduced for convenience and are used
│ for direct defined class functions. For example to define building
│ of the power class operator, the union and intersection operator and
│ the successor function. All these function constants can be
│ interpreted as abbreviations.
└
H = {h^k_i | i, k ∈ ω}, the s u b j e c t v a r i a b l e s V = {v_i | i ∈
ω}, as well as p r e d i c a t e v a r i a b l e s P = {p^k_i | i, k ∈ ω}.
┌
│ By ω we understand the natural numbers including zero. All involved
│ symbols are pairwise disjoint. Therefore we can conclude for
│ example: f^k_i = f^(k')_(i') → (k = k’ ∧ i = i’) and h^k_i ≠ v_j.
└
For the a r i t y or r a n k of an operator we take the upper index. The
set of predicate variables with zero arity is also called set of
p r o p o s i t i o n v a r i a b l e s or s e n t e n c e l e t t e r s
: A := {p_i⁰ | i ∈ ω }. For subject variables we write short hand certain lower
letters: v₁ = ‘u’, v₂ = ‘v’, v₃ = ‘w’, v₄ = ‘x’, v₅ = ‘y’, v₅ = ‘z’. Furthermore
we use the following short notations: for the predicate variables pⁿ₁ = ‘φ’ und
pⁿ₂ = ‘ψ’, where the appropriate arity n is calculated by counting the
subsequent parameters, for the proposition variables a₁ = ‘A’, a₂ = ‘B’ and a₃ =
C’, for the function variables: fⁿ₁ = ‘f’ und fⁿ₂ = ‘g’, where again the
appropriate arity n is calculated by counting the subsequent parameters. All
binary propositional operators are written in infix notation. Parentheses
surrounding groups of operands and operators are necessary to indicate the
intended order in which operations are to be performed. E. g. for the operator ∧
with the parameters A and B we write (A ∧ B). In the absence of parentheses the
usual precedence rules determine the order of operations. Especially outermost
parentheses are omitted. Also empty parentheses are stripped.
The operators have the order of precedence described below (starting with the
highest).
¬, ∀, ∃
∧
∨
→, ↔
The term t e r m is defined recursively as follows:
1. Every subject variable is a term.
2. Let i, k ∈ ω and let t₁, ..., t_k be terms. Then h^k_i(t₁, ..., t_k) is a
term and if k > 0, so f^k_i(t₁, ..., t_k) is a term too. Therefore all zero
arity function constants {h⁰_i | i ∈ ω} are terms. They are called
i n d i v i d u a l c o n s t a n t s .
┌
│ In an analogous manner subject variables might be defined as
│ function variables of zero arity. Because subject variables play an
│ important role they have their own notation.
└
We define a f o r m u l a and the relations f r e e and b o u n d subject
variable recursivly as follows:
1. Every proposition variable is a formula. Such formulas contain no free or
bound subject variables.
2. If p^k is a predicate variable with arity k and c^k is a predicate constant
with arity k and t₁, t₂, ..., t_k are terms, then p^k(t₁, t₂, ... t_k) and
c^k(t₁, t₂, ..., t_k) are formulas. All subject variables that occur at least
in one of t₁, t₂, ..., t_k are free subject variables. Bound subject
variables does not occur.
┌
│ This second item includes the first one, which is only listed for
│ clarity.
└
3. Let α, β be formulas in which no subject variables occur bound in one formula
and free in the other. Then ¬ α, (α ∧ β), (α ∨ β), (α → β) and (α ↔ β) are
also formulas. Subject variables which occur free (respectively bound) in α
or β stay free (respectively bound).
4. If in the formula α the subject variable x₁ occurs not bound
┌
│ This means that x₁ is free in the formula or does not occur at
│ all.
└
, then also ∀ x₁ α and ∃ x₁ α are formulas. The symbol ∀ is called
u n i v e r s a l q u a n t i f i e r and ∃ as e x i s t e n t i a l
q u a n t i f i e r . Except for x₁ all free subject variables of α stay
free. All bound subject variables are still bound and additionally x₁ is
bound too. All formulas that are only built by usage of 1. and 3. are called
formulas of the p r o p o s i t i o n a l c a l c u l u s .
For each formula α the following proposition holds: the set of free subject
variables is disjoint with the set of bound subject variables..
┌
│ Other formalizations allow for example ∀ x₁ α also if x₁ occurs
│ already bound within α. Also propositions like α(x₁) ∧ (∀ x₁ β) are
│ allowed. In this formalizations free and bound are defined for a
│ single occurrence of a variable.
└
If a formula has the form ∀ x₁ α respectively ∃ x₁ α then the formula α is
called the s c o p e of the quantifier ∀ respectively ∃.
All formulas that are used to build up a formula by 1. to 4. are called p a r t
f o r m u l a s .
___________________________________________________
Chapter 2
Axioms and Rules of Inference
═════════════════════════════
We now state the system of axioms for the predicate calculus and present the
rules for obtaining new formulas from them.
2.1 Axioms
――――――――――
The language of our calculus bases on the formalizations of D . H i l b e r t
, W . A c k e r m a n n [hilback], P . B e r n a y s and
P . S . N o v i k o v [novikov]. New rules can be derived from the herein
presented. Only these meta rules lead to a smooth flowing logical argumentation.
We want to present the axioms, definitions and rules in an syntactical manner
but to motivate the choosen form we already give some semantical
i n t e r p r e t a t i o n s .
The logical operators of propositional calculus ‘¬’, ‘∧’, ‘∨’, ‘→’ and ‘↔’
combine arbitrary p r o p o s i t i o n s to new propositions. A proposition
is a statement that affirms or denies something and is either „true” or „false”
(but not both).
┌
│ Later on we will define the symbols ⊤ and ⊥ as truth values.
└
The binary operator ‘∧’ (logical disjunction) combines the two propositions α
and β into the new proposition α ∧ β. It results in true if at least one of its
operands is true.
The unary operator ‘¬’ (logical negation) changes the truth value of a
proposition α. ¬ α has a value of true when its operand is false and a value of
false when its operand is true.
The l o g i c a l i m p l i c a t i o n ( i f ... t h e n ) the,
l o g i c a l c o n j u n c t i o n ( a n d ) and the l o g i c a l
e q u i v a l e n c e ( l o g i c a l b i c o n d i t i o n a l ) are
defined as abbreviations.
┌
│ Actually the symbols ∨, →, ↔ are defined later on and are a syntax
│ extension. But for convenience these symbols are already part of the
│ logical language.
└
The logical implication (‘if ... then’) could be defined as follows.
α → β :↔ ¬ α ∨ β
The logical conjunction (‘and’) could be defined with de Morgan.
α ∧ β :↔ ¬ (¬ α ∨ ¬ β)
The logical equivalence (‘iff’) is defined as usual.
α ↔ β :↔ (α → β) ∧ (β → α)
Now we come to the first axiom of propositional calculus. This axiom enables us
to get rid of an unnecessary disjunction.
☉ Axiom 1 (Disjunction Idempotence) [axiom:disjunction_idempotence]
(A ∨ A) → A
If a proposition is true, any alternative may be added without making it false.
☉ Axiom 2 (Axiom of Weakening) [axiom:disjunction_weakening]
A → (A ∨ B)
The disjunction should be commutative.
☉ Axiom 3 (Commutativity of the Disjunction) [axiom:disjunction_commutative]
(A ∨ B) → (B ∨ A)
An disjunction could be added at both side of an implication.
☉ Axiom 4 (Disjunctive Addition) [axiom:disjunction_addition]
(A → B) → ((C ∨ A) → (C ∨ B))
If something is true for all x, it is true for any specific y.
☉ Axiom 5 (Universal Instantiation) [axiom:universalInstantiation]
∀ x φ(x) → φ(y)
If a predicate holds for some particular y, then there is an x for which the
predicate holds.
☉ Axiom 6 (Existential Generalization) [axiom:existencialGeneralization]
φ(y) → ∃ x φ(x)
2.2 Rules of Inference
――――――――――――――――――――――
The following rules of inference enable us to obtain new true formulas from the
axioms that are assumed to be true. From these new formulas we derive further
formulas. So we can successively extend the set of true formulas.
☉ Rule 1 (Modus Ponens) [rule:modusPonens]
If both formulas α and α → β are true, then we can conclude that β is true as
well.
☉ Rule 2 (Replace Free Subject Variable) [rule:replaceFree]
We start with a true formula. A free subject variable may be replaced by an
arbitrary term, provided that the substituted term contains no subject variable
that have a bound occurrence in the original formula. All occurrences of the
free variable must be simultaneously replaced.
The prohibition to use subject variables within the term that occur bound in the
original formula has two reasons. First it ensures that the resulting formula is
well-formed. Secondly it preserves the validity of the formula. Let us look at
the following derivation.
∀ x ∃ y φ(x, y) → ∃ y φ(z,y) with axiom 5
∀ x ∃ y φ(x, y) → ∃ y φ(y,y) forbidden replacement: z in y, despite y
is already bound
∀ x ∃ y x ≠ y → ∃ y ≠ y replace ≠ for φ
This last proposition is not valid in many models.
☉ Rule 3 (Rename Bound Subject Variable) [rule:renameBound]
We may replace a bound subject variable occurring in a formula by any other
subject variable, provided that the new variable occurs not free in the original
formula. If the variable to be replaced occurs in more than one scope, then the
replacement needs to be made in one scope only.
☉ Rule 4 (Replace Predicate Variable) [rule:replacePred]
Let α be a true formula that contains a predicate variable p of arity n, let x₁,
..., x_n be subject variables and let β(x₁, ..., x_n) be a formula where x₁,
..., x_n are not bound. The formula β(x₁, ..., x_n) must not contain all x₁,
..., x_n as free subject variables. Furthermore it can also have other subject
variables either free or bound. If the following conditions are fulfilled, then
a replacement of all occurrences of p(t₁, ..., t_n) each with appropriate terms
t₁, ..., t_n in α by β(t₁, ..., t_n) results in another true formula.
1. the free variables of β(x₁, ..., x_n) without x₁, ..., x_n do not occur as
bound variables in α
2. each occurrence of p(t₁, ..., t_n) in α contains no bound variable of β(x₁,
..., x_n)
3. the result of the substitution is a well-formed formula
See III § 5 in [hilback].
The prohibition to use additional subject variables within the replacement
formula that occur bound in the original formula assurs that the resulting
formula is well-formed. Furthermore it preserves the validity of the formla.
Take a look at the following derivation.
φ(x) → ∃ y φ(y) with axiom 6
(∃ y y = y) ∧ φ(x) → ∃ y φ(y)
∃ y (y = y ∧ φ(x)) → ∃ y φ(y)
∃ y (y = y ∧ x ≠ y) → ∃ y y ≠ y forbidden replacment: φ(x) by x ≠ y,
despite y is already bound
∃ y x ≠ y → ∃ y y ≠ y
The last proposition is not valid in many models.
Analogous to rule 4 we can replace function variables too.
☉ Rule 5 (Replace Function Variable) [rule:replaceFunct]
Let α be an already proved formula that contains a function variable σ of arity
n, let x₁, ..., x_n be subject variables and let τ(x₁, ..., x_n) be an arbitrary
term where x₁, ..., x_n are not bound. The term τ(x₁, ..., x_n) must not contain
all x₁, ..., x_n. as free subject variables. Furthermore it can also have other
subject variables either free or bound. If the following conditions are
fulfilled we can obtain a new true formula by replacing each occurrence of σ(t₁,
..., t_n) with appropriate terms t₁, ..., t_n in α by τ(t₁, ..., t_n).
1. the free variables of τ(x₁, ..., x_n) without x₁, ..., x_n do not occur as
bound variables in α
2. each occurrence of σ(t₁, ..., t_n) in α contains no bound variable of τ(x₁,
..., x_n)
3. the result of the substitution is a well-formed formula
☉ Rule 6 (Universal Generalization) [rule:universalGeneralization]
If α → β(x₁) is a true formula and α does not contain the subject variable x₁,
then α → (∀ x₁ (β(x₁))) is a true formula too.
☉ Rule 7 (Existential Generalization) [rule:existentialGeneralization]
If α(x₁) → β is already proved to be true and β does not contain the subject
variable x₁, then (∃ x₁ α(x₁)) → β is also a true formula.
The usage and elimination of abbreviations and constants is also an inference
rule. In many texts about mathematical logic these rules are not explicitly
stated and this text is no exception. But in the exact QEDEQ format
corresponding rules exist.
___________________________________________________
Chapter 3
Derived Propositions
════════════════════
Now we derive elementary propositions with the axioms and rules of inference of
chapter chapter4.
3.1 Propositional Calculus
――――――――――――――――――――――――――
At first we look at the propositional calculus.
To define the predicate t r u e we just combine a predicate and its negation.
☉ Definition 1 (True) [definition:True]
⊤ :↔ A ∨ ¬ A
For a precise definition we should have written something like p⁰₀ = ⊤ and ⊤ :↔
(A ∨ ¬ A).
┌
│ In the deeper laying (see
│ http://www.qedeq.org/current/doc/project/qedeq_logic_language_en.pdf )
│ formal language this predicate has the name T R U E and zero
│ arguments. So we just have to map names to natural numbers to
│ fulfill the exact definition.
└
In the future we only write the symbol itself. It’s arity should be evident
from the formula.
For the predicate f a l s e we just negate t r u e .
┌
│ Analogous to the preceeding definition we can set p⁰₁ = ⊥
└
☉ Definition 2 (False) [definition:False]
⊥ :↔ ¬ ⊤
We have the following basic propositions.
☉ Proposition 1 (Basic Propositions) [theorem:propositionalCalculus]
(aa) ⊤
(ab) ¬ ⊥
(ac) A → A
(ad) A ↔ A
(ae) (A ∨ B) ↔ (B ∨ A)
(af) (A ∧ B) ↔ (B ∧ A)
(ag) (A ∧ B) → A
(ah) (A ↔ B) ↔ (B ↔ A)
(ai) (A ∨ (B ∨ C)) ↔ ((A ∨ B) ∨ C)
(aj) (A ∧ (B ∧ C)) ↔ ((A ∧ B) ∧ C)
(ak) A ↔ (A ∨ A)
(al) A ↔ (A ∧ A)
(am) A ↔ ¬ ¬ A
(an) (A → B) ↔ (¬ B → ¬ A)
(ao) (A ↔ B) ↔ (¬ A ↔ ¬ B)
(ap) (A → (B → C)) ↔ (B → (A → C))
(aq) ¬ (A ∨ B) ↔ (¬ A ∧ ¬ B)
(ar) ¬ (A ∧ B) ↔ (¬ A ∨ ¬ B)
(as) (A ∨ (B ∧ C)) ↔ ((A ∨ B) ∧ (A ∨ C))
(at) (A ∧ (B ∨ C)) ↔ ((A ∧ B) ∨ (A ∧ C))
(au) (A ∧ ⊤) ↔ A
(av) (A ∧ ⊥) ↔ ⊥
(aw) (A ∨ ⊤) ↔ ⊤
(ax) (A ∨ ⊥) ↔ A
(ay) (A ∨ ¬ A) ↔ ⊤
(az) (A ∧ ¬ A) ↔ ⊥
(ba) (⊤ → A) ↔ A
(bb) (⊥ → A) ↔ ⊤
(bc) (A → ⊥) ↔ ¬ A
(bd) (A → ⊤) ↔ ⊤
(be) (A ↔ ⊤) ↔ A
(bf) ((A → B) ∧ (B → C)) → (A → C)
(bg) ((A ↔ B) ∧ (C ↔ B)) → (A ↔ C)
(bh) ((A ∧ B) ↔ (A ∧ C)) ↔ (A → (B ↔ C))
(bi) ((A ∧ B) ↔ (A ∧ ¬ B)) ↔ ¬ A
(bj) (A ↔ (A ∧ B)) ↔ (A → B)
(bk) (A → B) → ((A ∧ C) → (B ∧ C))
(bl) (A ↔ B) → ((A ∧ C) ↔ (B ∧ C))
(bm) (A ∧ (A → B)) → B
(bn) (A ∧ (A → B)) ↔ (A ∧ B)
3.2 Predicate Calculus
――――――――――――――――――――――
For predicate calculus we achieve the following propositions.
We have the following basic propositions.
☉ Proposition 2 (Basic Propositions) [theorem:predicateCalculus]
(a) ∀ x (φ(x) → ψ(x)) → (∀ x φ(x) → ∀ x ψ(x))
(b) ∀ x (φ(x) → ψ(x)) → (∃ x φ(x) → ∃ x ψ(x))
(c) ∀ x (φ(x) ↔ ψ(x)) → (∀ x φ(x) ↔ ∀ x ψ(x))
(d) ∃ x (φ(x) ∧ ψ(x)) → (∃ x φ(x) ∧ ∃ x ψ(x))
(e) (∀ x ψ(x) ∨ ∀ x ψ(x)) → ∀ x (φ(x) ∨ ψ(x))
(f) ∃ x (φ(x) ∨ ψ(x)) ↔ (∃ x φ(x) ∨ ∃ x ψ(x))
(g) ∀ x (φ(x) ∧ ψ(x)) ↔ (∀ x φ(x) ∧ ∀ x ψ(x))
(h) ∀ x ∀ y φ(x, y) ↔ ∀ y ∀ x φ(x, y)
(i) ∃ x ∃ y φ(x, y) ↔ ∃ y ∃ x φ(x, y)
(j) ∀ x (φ(x) → A) → (∀ x φ(x) → A)
(k) ∀ x (A → φ(x)) ↔ (A → ∀ x φ(x))
(l) ∀ x (φ(x) ∧ A) ↔ (∀ x φ(x) ∧ A)
(m) ∀ x (φ(x) ∨ A) ↔ (∀ x φ(x) ∨ A)
(n) ∀ x (φ(x) ↔ A) → (∀ x φ(x) ↔ A)
(o) ∀ x (φ(x) ↔ ψ(x)) → (∀ x φ(x) ↔ ∀ x ψ(x))
3.3 Derived Rules
―――――――――――――――――
Beginning with the logical basis logical propositions and metarules can be
derived an enable a convenient argumentation. Only with these metarules and
additional definitions and abbreviations the mathematical world is unfolded.
Every additional syntax is c o n s e r v a t i v e . That means: within
extended system no formulas can be derived, that are written in the old syntax
but can not be derived in the old system. In the following such conservative
extensions are introduced.
☉ Rule 8 (Replace by Logical Equivalent Formula) [rule:replaceEquiFormula]
Let the formula α ↔ β be true. If in a formula δ we replace an arbitrary
occurence of α by β and the result γ is also a formula
┌
│ During that substitution it might be necessary to rename bound
│ variables of β.
└
and contains all the free subject variables of δ, then δ ↔ γ is a true formula.
☉ Rule 9 (Replacement of ⊤ by already derived formula)
[rule:replaceTrueByTrueFormula]
Let α be an already derived true formula and β a formula that contains ⊤. If we
get a well formed formula γ by replacing an arbitray occurence of ⊤ in β with α
then the following formula is also true: β ↔ γ
☉ Rule 10 (Replacement of already derived formula by ⊤)
[rule:replaceTrueFormulaByTrue]
Let α be an already derived true formula and β a formula that contains α. If we
get a well formed formula γ by replacing an arbitray occurence of α in β by ⊤
then the following formula is also true: β ↔ γ
☉ Rule 11 (Derived Quantification) [rule:derivedQuantification]
If we have already derived the true formula α(x) and x is not bound in α(x) then
the formula ∀ x α(x) is also true.
☉ Rule 12 (General Associativity) [rule:generalAssociativity]
If an operator of arity two fulfills the associative law it also fulfills the
general associative law. The operator can be extended to an operator of
arbitrary arity greater one. For example: instead of (a + b) + (c + d) we simply
write a + b + c + d.
┌
│ The operator of arity n is defined with a certain bracketing, but
│ every other bracketing gives the same result.
└
☉ Rule 13 (General Commutativity) [rule:generalCommutativity]
If an operator fulfills the general associative law and is commutative then all
permutations of parameters are equal or equivalent.
┌
│ That depends on the operator type: term or formula operator.
└
For example we have: a + b + c + d = c + a + d + b.
☉ Rule 14 (Deducible from Formula) [rule:definitionDeductionFromFormula]
We shall say that the formula β is d e d u c i b l e f r o m t h e
f o r m u l a α if the formula β from the totality of all true formulas of
the predicate calculus and the formula α by means of application of all the
rules of the predicate calculus, in which connection both rules for binding by a
quantifier, the rules for substitution in place of predicate variables and in
place of free subject variables must be applied only to predicate variables or
subject variables which do not occur in the formula α and α → β is a formula.
Notation: α ⊢ β.
That a formula β is deducible from th formula α must be strictly distinguished
from the deduction of a true formula from the axioms of the predicate calculus.
In the second case more derivation rules are available. For example if A is
added to the axioms then the formula B can be derived. But B is not deducible
from A.
☉ Rule 15 (Deduction Theorem) [rule:deductionTheorem]
If the formula β is deducible from the formula α, then the formula α → β can be
derived from the predicate calculus.
___________________________________________________
Chapter 4
Identity
════════
Everything that exists has a specific nature. Each entity exists as something in
particular and it has characteristics that are a part of what it is. Identity is
whatever makes an entity definable and recognizable, in terms of possessing a
set of qualities or characteristics that distinguish it from entities of a
different type. An entity can have more than one characteristic, but any
characteristic it has is a part of its identity.
4.1 Identity Axioms
―――――――――――――――――――
We start with the identy axioms.
We define a predicate constant of arity two that shall stand for the identity of
subjects.
☉ initial Definition 3 (Identity) [definition:identity]
x = y
For convenience we also define the negation of the identity a predicate
constant.
☉ Definition 4 (Not Identical) [definition:notEqual]
x ≠ y :↔ ¬ x = y
☉ Axiom 7 (Reflexivity of Identity) [axiom:identityIsReflexive]
x = x
☉ Axiom 8 (Leibniz’ replacement) [axiom:leibnizReplacement]
x = y → (φ(x) → φ(y))
☉ Axiom 9 (Symmetrie of identity) [axiom:symmetryOfIdentity]
x = y → y = x
☉ Axiom 10 (Transitivity of identity) [axiom:transitivityOfIdentity]
(x = y ∧ y = z) → x = z
We can reverse the second implication in the Leibniz replacement.
☉ Proposition 3 [theorem:leibnizEquivalence]
x = y → (φ(x) ↔ φ(y))
☉ Proposition 4 [theorem:identyImpliesFunctionalEquality]
x = y → f(x) = f(y)
4.2 Restricted Quantifiers
――――――――――――――――――――――――――
Every quantification involves one specific subject variable and a domain of
discourse or range of quantification of that variable. Until now we assumed a
fixed domain of discourse for every quantification. Specification of the range
of quantification allows us to express that a predicate holds only for a
restricted domain.
At the following definition the replacement formula for α(x) must „reveal” its
quantification subject variable. This is usually the first following subject
variable.
┌
│ For example: in the following formula we identify the subject
│ variable m for the second quantification: ∀ n ∈ ℕ ∀ m ∈ n m < n.
└
In the exact syntax of the QEDEQ format
┌
│ Again see http://www.qedeq.org/current/xml/qedeq/ .
└
the quantification subject variable is always given.
☉ Axiom 11 (Restricted Universal Quantifier)
[axiom:restrictedUniversalQuantifier]
∀ α(x) β(x) ↔ ∀ x (α(x) → β(x))
A matching definiton for the restricted existential quantifier is the following.
┌
│ Matching because of ¬ ∀ ψ(x) (φ(x)) ↔ ∃ x ¬ (ψ(x) → φ(x)) ↔ ∃ x
│ (ψ(x) ∧ ¬φ(x)) ↔ ∃ ψ(x) (¬φ(x)).
└
☉ Axiom 12 (Restricted Existential Quantifier)
[axiom:restrictedExistentialQuantifier]
∃ α(x) β(x) ↔ ∃ x (α(x) ∧ β(x))
For restricted quantifiers we find formulas according to Proposition
proposition 2.
+++
To express the existence of only one individuum with a certain property we
introduce a new quantifier.
☉ Axiom 13 (Restricted Uniqueness Quantifier)
[axiom:restrictedUniquenessQuantifier]
∃! α(x) β(x) ↔ ∃ α(x) (β(x) ∧ ∀ α(y) (β(y) → x = y))
[Term Definition by Formula]rule:termdef If the formula ∃! x α(x) holds, we can
expand the term syntax by D(x, α(x)). May the formula alpha(x) doesn’t contain
the variable y and let β(y) be a formula that doesn’t contain the variable x.
Then we define a new formula β(D(x, α(x))) by β(y) ∧ ∃! x (α(x) ∧ x = y). Also
in this abbreviate notation the subject variable x counts as bound, the subject
variable y is arbitrary (if it fulfills the given conditions) and will be
ignored in the abbreviation. Changes in α that lead to another formula α’
because of variable collision with β must also be done in the abbreviation. All
term building rules are extended accordingly. The expression is also replaceble
by ∃! y (β(y) ∧ α(y) or by β(y) ∧ α(y).
___________________________________________________
Bibliography
════════════
[witheruss] A . N . W h i t e h e a d , B . R u s s e l l , Principia
Mathematica,
Cambridge University Press, London 1910
[bernays] P . B e r n a y s , Axiomatische Untersuchung des Aussagen-Kalkuls
der
„Principia Mathematica”, Math. Zeitschr. 25 (1926), 305-320
[hilback] D . H i l b e r t , W . A c k e r m a n n , Grundzüge der
theoretischen
Logik, 2nd ed., Berlin: Springer, 1938. English version: Principles of
Mathematical Logic, Chelsea, New York 1950, ed. by R. E. Luce. See also
http://www.math.uwaterloo.ca/~snburris/htdocs/scav/hilbert/hilbert.html
[novikov] P . S . N o v i k o v , Elements of Mathematical Logic, Edinburgh:
Oliver and
Boyd, 1964.
[mendelson] E . M e n d e l s o n , Introduction to Mathematical Logic, 3rd.
ed.,
Belmont, CA: Wadsworth, 1987.
[guenter] V . G ü n t h e r , Lecture „Mathematik und Logik”, given at the
University of
Hamburg, 1994/1995.
[meyling] M . M e y l i n g , Hilbert II, Presentation of Formal Correct
Mathematical
Knowledge, Basic Concept,
http://www.qedeq.org/current/doc/project/qedeq_basic_concept_en.pdf .
QEDEQ modules that use this one:
qedeq_set_theory_v1
http://www.qedeq.org/0_04_01/doc/math/qedeq_set_theory_v1.xml