Re: Current Issues in the Philosophy of Practice of Mathematics & Informatics

[Thomas Streicher <streicher@mathematik.tu-darmstadt.de>]

> 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/ ]