System T⁰ (Thomas) [T superscript 0]

Notes

Decision procedure published by Ivo Thomas [Thomas, 1964, p320]

Based on

The system T⁰ (T superscript 0) is S1⁰ plus any axiom of the form LLa where a is a PC thesis. [Zeman, 1973, p281]

The system T⁰is therefore:

• Definitions
  • ?
• Rules
  • Uniform substitution (US)
  • Strict detachment (MP=>)
  • Adjunction (given a, b, return a&b) (AD)
  • substitution of strict equivalents. (EQS)
• Axioms
  • M1: (p&q)=>(q&p)
  • M2: (p&q)=>p
  • M3: ((p&q)&r)=>(p&(q&r))
  • M4: p=>(p&p)
  • M5: ((p=>q)&(q=>r))=>(p=>r)
  • LL(p>p) [Or LL any other PC thesis.]

[Zeman, 1973, p281]

Basis for

T = T⁰ + Axiom M6: p=>Mp [Zeman, 1973, p281]

T^x = T⁰ + axiom MLp [Feys, 1965, p122]

Go to ...

• Systems Page
• Structures Page
• Logic Page
• John Halleck's home page

© Copyright 2000, by John Halleck, All Rights Reserved.
This page is http://www.cc.utah.edu/~nahaj/logic/structures/systems/t-0.html
This page was last modified on January 24th, 2007