In logic we typically have signatures, terms, sentences, structured sets of sentences, entailment, models, satisfactions, axioms, theories and proof calculi. We cannot e.g. define entailment before we have a notion of sentences, and we should not define sentences before we have a notion of terms. The latter is a bit more controversial. In first-order logic I would see P(x), where P is a "predicate symbol", as a term, and not as a sentence, whereas putting a quantifier in front of it, Ex.P(x), makes it no longer a term. This is why I have difficulties e.g. to accept that the two 'not's in expressions like "not Ex.P(x)" and "Ex.not P(x)" would be the same. I am starting to think they are only informal as symbols, a bit similar as Church said lambda is and informal symbol, so actually not part of the formal syntax. Am I wrong or am I wrong?
I don't understand why atomic formulas are terms but not formulas. Always thought the Lawvere's hyperdoctrines made all this very clear: terms are in the base and formulas are in the fibres. In case there is a generic family of propositions A:Prop |- True(A) we can turn predicates into terms of type Prop. That's the shift to HOL. The 2 different negations are just negations in two different fibres. Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]