🚀 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

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

boshuck@triples.math.mcgill.ca (William Boshuck) writes:

* 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).

Pretty good so far...

* 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. 

But not here.  

It's not that it's in *error*, but just that it's not
so general.  There are plenty of good logics (like R,
R-W, Linear Logic, and so on), that satisfy modus ponens
and the deduction theorem (in the way you describe), 
but that don't validate the move:

	 A |- C
	--------  (Weakening; or K)
	A,B |- C

which you need (in some form) to get from T |- ~F to 
T,F |- F & ~F.

The reason you might want to get rid of the offending
principle is to invalidate the offensive

	 |- C
	-------
	|- B->C

which is invalid in all of the systems mentioned above,
and frankly, which *ought* to be invalid, on many sensible
readings of `->'.

Relevantly yours,

Greg Restall


--
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
Greg Restall        Philosophy Department, University of Queensland.   
gar@cltr.uq.oz.au   Queensland, 4072.  Australia.		         
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
The day logic stops being fun is the day it ceases to be my profession.
							   -- Bob Meyer