◄
Chapter
1 ◄
Index Chapter
3 ►
Beyond
Gödel
Simply
consistent constructive systems of first order Peano’s Arithmetic that do not
yield undecidable propositions by Gödel’s reasoning
(A compiled copy of Chapters 1 to 6 can be downloaded as a .pdf file from http://arxiv.org/abs/math/0201059.)
Chapter
2. Why is first order Arithmetic not omega-constructive?
Contents
2.0. Introduction
2.1. The Representation Theorem
2.2. What is the formal representation of f(x, y) in PA?
2.3.
Gödel’s Beta function
2.4. Can F(x, y, z) create a logical paradox in PA?
2.5. The ‘Liar’ paradox
2.6. The ‘Russell’ paradox
2.7. Creation through definition
2.8. When can PA+F(x1, x2, x3) be
assumed consistent?
2.9. What does PA prove constructively by (E1x3)F(k, m, x3)?
2.10. Mendelson’s proof of “PA proves: (E1x3)F(k, m, x3)”
2.11. What does (E1x3)F(x1, x2, x3) assert?
2.12. The introduction of Platonism into PA
2.13. How does PA prove the Platonistic
assertion (E1x3)F(x1, x2, x3)?
2.14. At which point does Platonism enter PA
formally?
2.15. Is PA necessarily Platonistic?
2.16. Is every model of PA necessarily
infinite, but not denumerable?
2.17. Is there a constructive PA?
In this second section we locate
specific non-constructivity
in PA and trace it to the
particular closed
Induction axiom
schema of PA,
and the strong
Generalisation rule
of inference of first order predicate calculus.
2.1. The
Representation Theorem
We start by noting that, in the
argument that a simply
consistent PA
cannot be omega-constructive,
the only overt assumptions (cf.
Gödel
1931 p190-191) were that the axioms and rules of inference of PA are recursively definable, and Podnieks
Representation Theorem (Section
3.3).
The constructive nature of the first assertion
is easily established from first principles by direct examination of the 45 functions and
relations defined recursively
by Gödel (cf.
Gödel
1931 p182-186).
We thus take a closer look at the
second assertion that every Turing-computable function
f(x, y) can be represented by a PA formula F(x, y, z) such that, for every set of natural numbers k, m, n, if f(k, m) = n then:
(ii) PA proves: (Az)(~(z=n) => ~F(k, m, z)).
2.2. What is
the formal representation of f(x, y) in PA?
Assuming that a function is Turing-computable if
and only if it is recursive,
we consider the case where f(x, y) is a recursive function,
defined by:
(i) f(x, 0) = g(x),
(ii) f(x, (y+1)) = h(x, y, f(x, y)),
(iii) where g(x1) and h(x1, x2, x3) are recursive functions
of lower rank[1] that are represented in PA by well-formed formulas G(x1, x2) and H(x1, x2, x3, x4).
Now Mendelson shows (p131 & p132)
that f(x1, x2) is represented
by the well-formed formula F(x1, x2, x3):
(Eu)(Ev)[((Ew)(Bt(u, v, 0,
w) & G(x1, w))) & Bt(u, v, x2, x3) &
(Aw)(w< x2 =>
(Ey)(Ez)(Bt(u, v, w, y) &
Bt(u, v, (w+1),
z) & H(x1, w, y, z))].
2.3. Gödel’s Beta function
Defining
Gödel’s Beta-function[2], β(x1, x2, x3) = rm(1+( x3+ 1).x2, x1), where rm(x, y) is the remainder
obtained on dividing y by x, the well-formed formula Bt(x1, x2, x3, x4) in §2.2 above
is a representation
in PA of β(x1, x2, x3), and is the well-formed formula (Mendelson p131):
(Ew)( x1 = ((1 + (x3 + 1). x2).w + x4) & (x4 < 1 + (x3 + 1). x2)).
2.4. Can F(x, y, z) create a
logical paradox in PA?
Having represented f(x, y) in PA by F(x, y, z) for every set of natural numbers k, m, n such that f(k, m) = n, the question arises: Is the well-formed formula F(x, y, z) well-defined
in PA?
In other words, can we ensure that
the recursive
predicate f(x, y) has not
been represented
by tacitly postulating a well-formed formula
F(x, y, z) of PA as well-defined, which may implicitly admit
the possibility of a formal
logical paradox
in PA?
To see the significance of this
question, we review the earlier paradox, loosely ascribed to Epimenides,
which arises obviously if we introduce by definition a ‘Liar’
expression, which reads as “The ‘Liar’ proposition is a lie”, as a valid proposition
within the language in which the expression is constructed.
Clearly the grammar of an ordinary
language, which governs the construction of words and propositions of the language for use as a
means of general unrestricted communication, does not contain the specification
necessary to prohibit the creation by definition of such vague,
or ill-defined, self-referential expressions that have the formal form of
a proposition,
but which are devoid of both communicative content and meaning.
Russell’s expression, within set
theory, for a set ‘Russell’ whose elements are all, and only, those sets
of the Theory that do not belong to themselves, is equally paradoxical.
Here also the axioms and
logical rules of
inference of the theory, which govern the construction of sets for
use in a more restricted and precise language of mathematical communication, do
not contain the specification necessary to satisfactorily prohibit the creation
by definition of vague,
ill-defined or inconsistent
entities that apparently harbour concealed concepts involving unruly infinite sets.
2.7. Creation
through definition
We note that definitions are
essentially arbitrary assignments of convenient names within a language or
theory for expressing complex reasoning in a compact, more readable, and easier
to grasp form.
The paradoxes indicate that unrestricted
definitions may admit creation of well-formed expressions within the language
or theory that lead to an inconsistency.
Clearly such expressions must be considered as ill-defined within the language
or theory.
It follows that a language or
theory that admits such well-formed expressions as well-defined cannot be reasonably assumed
to be simply consistent.
2.8.
Well-defined well-formed formulas of PA
Now the formal response towards the containment (as
distinct from the resolution) of such paradoxes in PA appears to be the implicit
thesis that if a well-formed formula is provable in PA, then it necessarily represents a function or predicate that
is well-defined
in PA.
We may, therefore, reasonably
assume that such well-formed formulas do not affect the formal consistency of
the axioms
of PA.
Thus, to ensure that F(x1, x2, x3) does
not introduce an inconsistency
in PA, Mendelson argues (p134) that F(x1, x2, x3) strongly represents
f(x1, x2) in PA, in the sense that:
PA proves:
(E1x3)F(x1, x2, x3),
where ‘E1x3’ defines
uniqueness (Mendelson
p79).
However, in the light of our
argument in the preceding paragraph, if F(x1, x2, x3) admits
construction of well-formed formulas in PA that translate, under interpretation,
as circular, ill-defined or vaguely defined predicates such as those that lead to the
logical antinomies, then the strong
representability of F(x1, x2, x3) in PA provides reasonable grounds
for arguing that PA is itself an ill-defined
system.
2.9. What does PA prove constructively by (E1x3)F(k, m, x3)?
We therefore consider in some detail
the significance of the formal
provability,
in PA, of the well-formed formula (E1x3)F(k, m, x3) for any given numerals k, m:
PA proves:
(E1x3)(Eu)(Ev)[((Ew)(Bt(u, v, 0,
w) & G(k, w))) &
Bt(u, v, m, x3) & (Aw)(w< m => (Ey)(Ez)(Bt(u, v, w, y) &
Bt(u, v, (w+1),
z) & H(k, w, y, z))].
Now “PA proves: (E1x3)F(k, m, x3)” intuitively asserts that, for any given natural numbers
k, m, we can construct
natural numbers
x3 (uniquely),
u, v that
define a Beta-function
such that β(u, v, 0) = g'(k) and, for all i<m, β(u, v, i) = h'(k, i, f'(k, i)), and β(u, v, m) = x3, where f'(x1, x2), g'(x1) and h'(x1, x2, x3) are any
recursive functions
that are formally
represented
by F(x1, x2, x3), G(x1, x2) and H(x1, x2, x3, x4)
respectively such that:
(i) f'(k, 0) = g'(k),
(ii) f'(k, (y+1)) = h'(k, y, f'(k, y)) for all y<m,
(iii) g'(x1) and h'(x1, x2, x3) are recursive functions
that are assumed to be of lower rank than f'(x1, x2).
For any arbitrarily given sequence
of natural numbers
k0, k1, ... , kn, we can clearly determine an infinity of values of up, vp,
kp such that the Beta-function β(up, vp, i) = ki for all 0 =< i =< n, and β(up, vp, (n+1)) = kp.
Hence
the PA provability of (E1x3)F(k, m, x3) is simply the intuitive assertion that, for any
given natural numbers
k and m, we can always construct some (non-unique) pair of natural numbers
u, v such that
the Beta-function
β(u, v, i) represents the
first m terms, i.e. f'(k, 0), f'(k, 1), ... , f'(k, m), which are common to every primitive recursive function such as f'(x1, x2) that is
formally represented by F(x1, x2, x3).
We
can see that this is constructively
provable for any given natural
numbers
k and m since, given F(x1, x2, x3), we can determine a suitable Turing
machine to construct the sequence f'(k, 0), f'(k, 1), ... , f'(k, m) uniquely and verify the assertion.
We
note, however, that if g is the Gödel-number of any Turing-computable proof of (E1x3)F(k, m, x3) as above then, trivially, g>m.
We cannot thus conclude from the
above argument that there is necessarily a Turing-computable constructive proof of the existence of a PA-formula that
yields the non-terminating sequence f(k, 0), f(k, 1), ... , f(k, m), ..., which we
could therefore take as representing
the function f(k, y) uniquely.
2.10.
Mendelson’s proof of PA proves: (E1x3)F(k, m, x3)
The Turing-decidability of the assertion (E1x3)F(k, m, x3) is reflected in Mendelson’s proof of the above (p133),
which relies on an essentially constructive meta-induction argument as below that does
not appeal to strong
Generalisation:
(Am)[[PA proves: (E1x3)F(0,
m, x3)] =>
[PA proves: (E1x3)F(0,
m+1, x3)]]
(Am)[PA proves:
(E1x3)F(0, m, x3)]
(Ak)(Am)[[PA proves: (E1x3)F(k, m, x3)] => [PA
proves: (E1x3)F(k+1, m, x3)]]
(Ak)(Am)[PA proves: (E1x3)F(k, m, x3)]
2.11. What does (E1x3)F(x1, x2, x3) assert?
Turning next to the issue of strong representability,
we consider the meta-assertion:
PA proves:
(E1x3)(Eu)(Ev)[((Ew)(Bt(u, v, 0,
w) & G(x1, w))) & Bt(u, v, x2, x3) &
(Aw)(w< x2 => (Ey)(Ez)(Bt(u, v, w, y) &
Bt(u, v, (w+1),
z) & H(x1, w, y, z))].
Now “PA proves: (E1x3)F(x1, x2, x3)”
intuitively asserts that, for variable x1, x2, we can
similarly construct natural
numbers x3 (uniquely), u, v that
define a Beta-function
such that β(u, v, 0) = g'(x1) and, for all i =< x2, β(u, v, i) = h'(x1, i, f'(x1, i)), where f'(x1, x2), g'(x1) and h'(x1, x2, x3) are any
recursive functions
that are formally
represented
by F(x1, x2, x3), G(x1, x2) and H(x1, x2, x3, x4)
respectively such that:
(i) f'(x1, 0) = g'(x1),
(ii) f'(x1, (y+1)) = h'(x1, y, f'(x1, y)) for all y< x2,
(iii) g'(x1) and h'(x1, x2, x3) are recursive functions
that are assumed to be of lower rank than f'(x1, x2).
Hence
the PA provability of (E1x3)F(x1, x2, x3) interprets as
the intuitive assertion that, even for variable x1 and x2, we can determine
some pair of natural
numbers u, v such that the Beta-function β(u, v, i) represents any
indeterminate number, x2, of terms, i.e.
the sequence f'(x1, 0), f'(x1, 1), ... , f'(x1, x2), of every primitive
recursive function such as f'(x1, x2) that is
formally represented by F(x1, x2, x3).
2.12. The
introduction of Platonism into PA
In
other words, the PA provability of (E1x3)F(x1, x2, x3)
corresponds to the intuitive, non-constructive, assertion that there is (interpreted
Platonistically) some Beta-function β(u, v, i) that represents
the sequence f(x1, 0), f(x1, 1), ... , f(x1, x2) for any
unspecified, and indeterminate, length x2.
If
PA has any non-denumerable model, then the above is, essentially, the assertion that F(x1, x2, x3)
uniquely represents
f(x1, x2) in PA. It implicitly implies that
the non-terminating sequence of values f(x1, 0), f(x1, 1), ..., f(x1, x2), ... forms a well-defined totality, which
can be uniquely named and referenced in PA by some (unique up to isomorphism) Beta-function βf(u, v, i).
The PA provability of (E1x3)F(x1, x2, x3) thus
corresponds to a non-constructive
assertion of the Platonistic
existence of
such a totality.
2.13. How does PA prove the Platonistic assertion (E1x3)F(x1, x2, x3)?
The question arises: How, then,
does PA prove an essentially Platonistic
assertion such as (E1x3)F(x1, x2, x3)?
After establishing the argument by
which we can show that PA
proves: (E1x3)F(k, m, x3), Mendelson notes, indicating outlines of the proof (p134),
that, for primitive recursive functions (Mendelson p120):
“The
part of the proof given above to show that the recursion rule does not lead out
of the class of representable
functions can be strengthened to yield strong representability ...”
Mendelson’s indicated argument
appears to be that we can establish by meta-induction:
[PA proves: (E1x3)F(0,
x2, x3)] =>
[PA proves: (E1x3)F(0,
x2+1, x3)]
PA
proves: (E1x3)F(0,
x2, x3) =>
(E1x3)F(0, x2+1, x3)
PA
proves: (Ax2)(( E1x3)F(0,
x2, x3) =>
(E1x3)F(0, x2+1, x3)) ... Gen
PA
proves: (Ax2)( E1x3)F(0,
x2, x3) ... Induction
[PA proves: (Ax2)( E1x3)F(x1, x2, x3)] => [PA
proves: (Ax2)( E1x3)F(x1+1, x2, x3)]
PA
proves: (Ax2)( E1x3)F(x1, x2, x3) =>
(Ax2)( E1x3)F(x1+1, x2, x3)
PA
proves: (Ax1)((Ax2)(( E1x3)F(x1, x2, x3) =>
(Ax2)( E1x3)F(x1+1, x2, x3))
PA
proves: (Ax1)(Ax2)( E1x3)F(x1, x2, x3)
PA
proves: (E1x3)F(x1, x2, x3)
Assuming that this correctly
represents Mendelson’s intention, the validity of the above reasoning gives the
necessary validity to F(x1, x2, x3) as a well-defined
well-formed formula that is consistent with
the axioms
of PA.
2.14. At which
point does Platonism enter PA formally?
The
question arises: At which point does PA formalise Platonistic elements?
We note that, in the above
argument, the non-constructive
conclusions in the reasoning are those that arise from application of the closed Induction axiom schema (Mendelson p103)
and the strong
Generalisation rule
of inference of first
order predicate calculus (Mendelson p57):
(i) Closed
Induction : (F(0) & ((Ax)(F(x) =>
F(x+1))) =>
(Ax)(F(x)
(ii) Strong
Generalisation : (Axi)F(xi) follows
from F(xi)
These are the only assumptions
that can be objected to intuitionistically in the above argument to provide
legitimacy for F(x1, x2, x3) as a well-defined well-formed formula that is consistent with
the axioms
of PA.
2.15. Is PA
necessarily Platonistic?
The question arises: Assuming that
PA is simply consistent, does the above argument,
that PA is a non-constructive
system, imply
that PA is necessarily Platonistic?
To put the query in perspective,
we note that the meta-assertion:
intuitively
represents a denumerable
infinity of formal
statements:
where only the denumerable
terms that can be expressed in PA, such as k, are substituted for xi.
However, the meta-assertion:
is a single formal
assertion that, under interpretation
in a model
of PA, may translate into an infinitely-compound proposition
that is not necessarily denumerably-compound.
Since the two are formally
equivalent in the presence of strong Generalisation, the question is
then: Does strong
Generalisation formalise
Platonism[3] in PA?
2.16. Is every
model of PA necessarily infinite, but not denumerable?
The above equivalence in PA also raises the question: Is
every model
of PA necessarily, infinite but
not denumerable,
since PA is shown to contain formally non-constructive
elements.
As we have argued in §1.17
of the previous section “Chapter 1. First order Arithmetic is not omega-constructive”,
there is an in-built ambiguity
in the construction of PA
once it admits omega-provable propositions.
We then face the possibility of predicates
giving rise to well-defined
well-formed formulas in PA that may not faithfully
reflect our intuitive understanding of the natural numbers, but that are not obviously
transfinite
in nature.
This ambiguity, prima facie, does
not admit an unequivocal answer to the above question.
2.17. Is there
a constructive PA?
The question thus arises: Can we formally
represent our intuitive Arithmetic of the natural numbers less ambiguously, and more
faithfully?
We address this question in the
next section: Is there an omega-constructive first order Arithmetic?
◄ Index
◄ Contents ◄ Chapter 1 ▲Chapter 2
Chapter 3 ► Chapter
4 ► Chapter 5 ► Conclusions
► Web_links ►
(Updated : Friday 11th January 2002 2:31:41 AM by re@alixcomsi.com)
References
Burbanks, Andrew. (e-seminar)
Fast-Growing Functions and Unprovable Theorems.
<Home page : http://www.maths.bris.ac.uk/~maadb/>
<Seminar
: http://www.maths.bris.ac.uk/~maadb/research/seminars/online/fgfut/index.html>
<Ord’ls
: http://www.maths.bris.ac.uk/~maadb/research/seminars/online/fgfut/fgfut09.html>
Davis, M (ed.). 1965. The
Undecidable. Raven Press, New York.
<Home
page : http://www.cs.nyu.edu/cs/faculty/davism/>
Franzén, Torkel. Provability and
Truth.
< Home page : http://www.sm.luth.se/~torkel/>
<See also remarks : http://www.sm.luth.se/~torkel/eget/godel/system.html>
<See also remarks : http://www.sm.luth.se/~torkel/eget/thesis/chapter5.html>
Friedman, Harvey. 1997. Unprovable
theorems in discrete mathematics.
<Unprovable
: http://www.math.berkeley.edu/~ribet/Colloquium/friedman.html>
Gödel, Kurt.
1931. On formally undecidable propositions of Principia Mathematica and related
systems I. Also in M. Davis (ed.). 1965. The Undecidable. Raven Press, New
York.
<1931
Paper : http://www.ddc.net/ygg/etext/godel/godel3.htm>
<Formal system : http://www.ddc.net/ygg/etext/godel/godel3.htm
- 15>
<Reducibility : http://www.ddc.net/ygg/etext/godel/godel3.htm
- AXIOM-IV>
<Comprehension : http://www.ddc.net/ygg/etext/godel/godel3.htm
- AXIOM-IV>
<See remarks on p190/191 : http://www.ddc.net/ygg/etext/godel/godel3.htm
- 16>
<Recursive definitions : http://www.ddc.net/ygg/etext/godel/godel3.htm
- DEF1>
< Beta-function : http://www.ddc.net/ygg/etext/godel/godel3.htm
- LEMMA1>
< See remarks on p189 : http://www.ddc.net/ygg/etext/godel/godel3.htm
- 16>
<Eqn. 8.1 : http://www.ddc.net/ygg/etext/godel/godel3.htm
- EQ8.1>
<Axiom IV : http://www.ddc.net/ygg/etext/godel/godel3.htm
- AXIOM-IV>
<Footnote 48a : http://www.ddc.net/ygg/etext/godel/godel3.htm
- 48a>
<cf. Recursive definition #17 : http://www.ddc.net/ygg/etext/godel/godel3.htm
- DEF17>
<cf.
Proposition V : http://www.ddc.net/ygg/etext/godel/godel3.htm#PROP-V>
Gödel, Kurt. 1934. On undecidable propositions of formal
mathematical systems. In M. Davis (ed.). 1965. The Undecidable. Raven
Press, New York.
Lucas, J. R. The Gödelian
argument.
<Home
page : http://users.ox.ac.uk/~jrlucas/>
<Gödelian argument : http://www.leaderu.com/truth/2truth08.html>
Mendelson, Elliott. 1964. Introduction to Mathematical Logic. Van Norstrand,
Princeton.
<Home
page : http://sard.math.qc.edu/Web/Faculty/mendelso.htm>
Parikh, Rohit. 1973. On the length of proofs. In Trans. AMS, 177, 29-36
<Home
page : http://www.sci.brooklyn.cuny.edu/cis/parikh/>
Parsons, Charles D. 1995. Platonism
and mathematical intuition in Kurt Gödel's thought. In The Bulletin of Symbolic
Logic, Volume 1, Issue 1, March 1995.
<1995
Article : http://www.math.ucla.edu/~asl/bsl/0101-toc.htm>
Peregrin, Jaroslav. 1997. Language and its Models: Is Model Theory a Theory of Semantics?
< cf.
also Models : http://www.hf.uio.no/filosofi/njpl/vol2no1/models/models-html.html>
<cf.
also Quantifier : http://www.hf.uio.no/filosofi/njpl/vol2no1/models/node8.html>
<cf. also Basis : http://www.hf.uio.no/filosofi/njpl/vol2no1/models/node5.html>
< cf. also Consequence : http://www.hf.uio.no/filosofi/njpl/vol2no1/models/node11.html>
< cf. also Truth : http://www.hf.uio.no/filosofi/njpl/vol2no1/models/node3.html>
< cf. also Language : http://www.hf.uio.no/filosofi/njpl/vol2no1/models/node2.html>
Podnieks, Karlis. 2001. Around
Goedel's Theorem.
<Home
page : http://www.ltn.lv/~podnieks/index.html>
<Around
Goedel’s Theorem : http://www.ltn.lv/~podnieks/gt.html>
<Goedel's
Incompleteness Theorem : http://www.ltn.lv/~podnieks/gt5.html - BM5_3>
<Standard first order Arithmetic
PA : http://www.ltn.lv/~podnieks/gt3.html
- BM3>
<Formula-number : http://www.ltn.lv/~podnieks/gt5.html
- BM5_2>
<Decode : http://www.ltn.lv/~podnieks/gt5.html
- BM5_2>
<Representation theorem : http://www.ltn.lv/~podnieks/gt3.html
- BM3_3>
<Platonism : http://www.ltn.lv/~podnieks/gt1.html>
<Self-reference lemma : http://www.ltn.lv/~podnieks/gt5.html
- BM5_2>
Rosmaita, Brian J. Minds, machines,
and metamathematics: constraints on the mathematical objection to mechanism.
<Article : http://www.personal.kent.edu/~brosmait/apa96.html>
Web resources
Free On-line Dictionary of
Computing.
<Dictionary
: http://www.nightflight.com/foldoc/>
<cf.
constructive : http://lgxserve.ciseca.uniba.it/lei/foldop/foldoc.cgi?query=constructive>
<Simply
consistent : http://www.swif.uniba.it/lei/foldop/foldoc.cgi?simple+consistency>
<Infinite
: http://www.swif.uniba.it/lei/foldop/foldoc.cgi?query=infinite&action=Search>
<Generalisation
: http://www.swif.uniba.it/lei/foldop/foldoc.cgi?generalization>
<Converse
: http://lgxserve.ciseca.uniba.it/lei/foldop/foldoc.cgi?query=converse>
<Turing
machine : http://www.swif.uniba.it/lei/foldop/foldoc.cgi?query=turing>
<Artificial
Int. : http://www.swif.uniba.it/lei/foldop/foldoc.cgi?query=AI&action=Search>
<Range :
http://www.nightflight.com/foldoc-bin/foldoc.cgi?query=range>
<Cmprhn. axiom : http://ase.isu.edu/ase01_07/ase01_07/bookcase/ref_sh/foldoc/99/8.htm>
<ZF set
theory : http://ase.isu.edu/ase01_07/ase01_07/bookcase/ref_sh/foldoc/35/122.htm>
<Mapping
: http://www.swif.uniba.it/lei/foldop/foldoc.cgi?query=mapping&action=Search>
Free
On-line Dictionary of Philosophy.
<Dictionary : http://www.swif.uniba.it/lei/foldop/>
Glossary of First-Order Logic.
<Glossary
: http://www.earlham.edu/~peters/courses/logsys/glossary.htm>
<First
order : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- fot>
<Predicate calculus : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- pl>
<Arithmetic : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- arithmetic>
<Omega : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- omegacom>
<Formula : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- formalsystem>
<Domain : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- domain>
<Set : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- set>
<Natural numbers : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- naturals>
<Numeral : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- numeral>
<Compound : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- compoundprop>
<cf. Meta... : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- metalanguage>
<Intrprttn. : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- interpretation>
<Equivalent : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- equivalence>
<Omega-comp. : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- omegacom>
<Free variable : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- freevar>
<Consequence : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- syncon>
<Proof sequence : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- proof>
<Denum. : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- denumerableset>
<Rcrsv. : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- recursivefunction>
<Frml sys. : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- formallanguage>
<Cptbl. : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- computablefunction>
<Standard model : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- model>
<Set theory : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- settheory>
<Closure : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- closure>
<Model : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- model>
<Std. set theory : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- settheory>
<Epimenides
: http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- enumset>
<Russell : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- russellparadox>
<Gödel-number : http://www.earlham.edu/~peters/courses/logsys/glossary.htm#gnumbering>
<Well-formed formula : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- wff>
<Rprsntn. : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- repfunction>
<Proposition : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- proposition>
<Predicate : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- powerset>
<Rules of inf. : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- rulesinf>
<Total fn. : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- totalfunction>
<Satisfaction : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- satisfaction>
<Axioms : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- axioms>
<Function : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- function>
<Dcdbl : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- decidablesystem>
<Transfinite : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- totalfunction>
<Exstnc. pr. : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- existenceproof>
<Cnst. pr. : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- constructiveproof>
<Implication : http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- implication>
<Completeness
: http://www.earlham.edu/~peters/courses/logsys/glossary.htm
- completeness>
Internet
Encyclopedia of Philosophy
<Antinomies : http://www.utm.edu/research/iep/p/par-log.htm>
Larry
Hauser’s Mostly Modern Philosophical Glossary.
<Glossary : http://members.aol.com/lshauser2/lexicon.html>
<True : http://members.aol.com/lshauser2/lexicon.html
- truth>
MacTutor History of Mathematics
archive
<Home page : http://www-groups.dcs.st-and.ac.uk/~history/>
<Kurt Gödel : http://www-groups.dcs.st-and.ac.uk/~history/Mathematicians/Godel.html
>
<MathPages : http://www.mathpages.com/home/>
Stanford
Encyclopedia of Philosophy.
<Encyclopedia
: http://setis.library.usyd.edu.au/stanford/archives/win1997/contents.html>
<Vagueness : http://setis.library.usyd.edu.au/stanford/archives/win1997/entries/vagueness/>
<cf. also Non-constructive : http://plato.stanford.edu/entries/mathematics-constructive/
- 2>
<Intuitionistically : http://plato.stanford.edu/entries/logic-intuitionistic/>
<Principia : http://plato.stanford.edu/entries/principia-mathematica/>
<cf. also Constructive : http://plato.stanford.edu/entries/mathematics-constructive/
- 1>
<cf. also Platonism : http://plato.stanford.edu/entries/mathphil-indis/
- 1>
Web Dictionary of
Cybernetics and Systems
<Dictionary : http://pespmc1.vub.ac.be/ASC/indexASC.html>
<Isomorphism : http://pespmc1.vub.ac.be/ASC/ISOMORPHISM.html>
xrefer
<Home page : http://www.xrefer.com/>
<Axiom of reducibility : http://www.xrefer.com/entry/553361>