Re: SUO: Theory Query
Chris,
Yes, I admit that I meant aleph-1, since the set of all subsets of
formulas is indeed uncountable (and yes, I am assuming the continuum
hypothesis).
In comparing the size of the two lattices -- the lattice of all subsets
of formulas and the lattice of all deductively closed sets of formulas,
I meant that for every one of the latter, there are infinitely more
(in fact, uncountably more) of the former:
1. Every deductively closed set S is infinite, since if it contains p,
it also contains p and p, p or p, p and (p or p), p or (p and P)...
2. Any subset of these formulas can be deleted from S and the remainder
would still have S as its deductive closure.
3. Since there are uncountably many such possible deletions, the
number of sets that have S as their deductive closure must be
uncountably infinite.
4. Therefore, for every element S of the lattice of all deductively
closed sets, there are infinitely many elements of the lattice of
all subsets -- all of which have S as their deductive closure.
5. In fact, the lattice of all deductively closed sets is isomorphic
to the set of all equivalence classes of the set of all subsets
of formulas under the condition that U and V are in the same
equivalence class if they have the same deductive closure.
Point #5 characterizes the lattice of all deductively closed sets as
a quotient space.
CM> I think the nodes you want in your lattice are *deductively closed*
> sets of sentences.
Yes.
CM> The relation that gives rise to your lattice is then simply the
> subset relation.
No, because you can delete uncountably many sentences from any element
of the lattice while still staying within the same equivalence class.
Provability (or entailment, since we are talking about FOL) is the
relation that defines the partial ordering of the lattice: for any two
theories U and V, U<V iff V|-U (or V|=U) and there exists at least one
sentence in V that is not in U.
On the question of the proper use of the term "tautology":
1. We agree that all logical truths of propositional calculus
merit the term "tautology".
2. We also agree that all logical truths of predicate calculus
that are substitutional instances of a tautology by point #1
are also worthy of being called tautologies.
3. But we disagree on the question of whether it is appropriate
to use the term "tautology" for logical truths of predicate
calculus derived by other rules of inference.
I agree with you that most recent books on predicate calculus take
your position. But the usage was by no means settled earlier in the
20th century. One author who agrees with my usage is the author of
the Tractatus Logico-Philosophicus, and I believe that many other
logicians and philosophers adopted his usage.
I agree that the following statement accurately characterizes current
usage in many textbooks (perhaps even all recent ones):
CM> Tautologies are logical truths that depend for their truth
> value ultimately only on the meanings of their propositional
> connectives. (This can be made as precise as you please.) Logical
> truths include those that depend in addition upon on the meanings of
> their quantifiers. Note also that the distinction is actually
> appealed to in many standard presentations of predicate logic: rather
> than providing an axiomatization for the propositional part, some
> logicians simply include "all tautologies" as axioms.
However, most authors of current textbooks on logic are abysmally
ignorant of the history of their own subject and of the best available
axiomatizations for logic. I have never seen a single textbook (other
than mine) that adopts Peirce's rules of inference, which every logician
who has ever seen them admits are the most general and elegant rules
of inference ever proposed for FOL. (And they also have generalizations
to other logics as well.)
In Peirce's system, the same three rules are used for both propositional
and predicate logic. And none of those three rules use substitution
for propositional variables -- because the system has no variables.
So the distinction you are proposing depends on features of just one
rather clunky system of inference.
For a tutorial on Peirce's system written by CSP himself (with my
annotations), see
http://www.jfsowa.com/peirce/ms514.htm
John