|
|
William Elliot wrote:
On Wed, 25 Oct 2006, Atreides wrote:
F is a set of sentences: { A_1, A_2, ...} s.t. {A_1 .. A_i} |/= A_i+1 (
A_i+1 is not a logical consequence of previous A_i's).
|- means logical consequence, provable.
T |= A means that A is a logical consequence of T, i.e. A is true in all
models of T. T |- A means that A is provable from T. In case of first
order logic these two notions coincide.
As David already pointed out, from Atreides's assumption it doesn't
follow that F is not finitely axiomatizable. For example, let c be some
fixed constant symbol and let A_1 be the conjunction of the usual axioms
for the successor function and let A_i for i > 1 be SS...S0 =/= c with
i-1 S's. The finite set of sentences consisting of the usual axioms for
the successor function together with
0 =/= c
for all x(Sx =/= c --> SSx =/= c)
then has the same deductive closure as {A_1, A_2, ...} even though {A_1,
... , A_i} |/- A_i+1 for all i.
How to prove that F is NOT finite axiomatizable?
{ (Ex)~(x = x) } is a finite collection of statements that will prove
every statement in F.
Certainly. But it isn't an axiomatization of F unless F is inconsistent.
--
Aatu Koskensilta (aatu.koskensilta@xxxxxxxxx)
"Wovon man nicht sprechen kann, daruber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
|
|