🚀 go-pugleaf

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