🚀 go-pugleaf

In article <1992Jul22.205827.16651@cenatls.cena.dgac.fr> alliot@cenatls.cena.dgac.fr (Jean-Marc Alliot) writes:
>
>Consistency: A system is consistent if, for any wff F, we
>can not have at the same time (F is a theorem) and (not F is a
>theorem). 
>
>Categoricity: a system is categoric if, for any wff F, we have either
>(F is theorem) or (not F is a theorem).
>
>Strong completeness: a system based on a set S of axioms is strongly
>complete if for any wff F, we have either (F is a theorem) or (F added
>to S is an inconsistent system).
>
>
>Now the questions:
>
>1) It seems quite clear that in any system which is a superset of
>propositional calculus Categoricity and Strong completeness are
>equivalent. However a short and clear demonstration would be very much
>welcome.
>
>2) Does the property hold in the general case (I especially think of
>intuitionist logic) ?
>

The proof which answers question 1) depends on something
called the deduction theorem which, in turn gives an answer to
the second question. The deduction theorem says that for a
theory T and formulas F,G, that the following inferences (both
top to bottom and bottom to top) are valid

                T,F |- G
              ------------
              T |- F ==> G   .	

(I am using |- to denote provability in whatever logic is
under consideration) In some treatments of logic, this is
virtually the definition of implication (perhaps rightly so).
In particular, this rule is valid in intuitionistic, and modal
logics (at least in the more common ones like S4).

If T is a theory in a logic which admits the above rule for
implication then we can say the following. First, categoricity
implies strong completeness: Suppose T is categorical. If T |-
F then that's it. Otherwise, T |- ~F in which case T,F |- F &
~F so T adjoin F is an inconsistent theory. Now, strong
completeness implies categoricity: Again, if F is a theorem
then you're done.  Otherwise, T adjoin F is an inconsistent
theory; that is, T,F |- (false). By the above rule we get
T |- F ==> (false), that is, T |- ~F. 

I hope this has been helpful.

WHB