Independence of Tarski's law in Henkin's propositional fragments.
Ivo Thomas · Notre Dame Journal of Formal Logic · 1960
The system {A1-3, ( ' in which x* is x. or x .3 y (with y a new variable) in the /-th schema according as %ι is T or F in the -th valuation (according to some ordering) of *m) 3y according as V ?(Λ; 1 , . . ., x m ) is T or F. (Henkin used x( ~^y ^)y in place of our antecedents #j, but since A 3 .B 3 C a fl d ^DC^^^.BDC are equivalent forms in any system containing Al-2, we use the shorter expression.)<pis a function symbol, but we shall usually refrain from indicating its argument places, and this should not cause confusion.L'Abbe in [2] showed that only the independence of A3 is ever in doubt.We here show the general (necessary and sufficient) conditions for A3 to be independent 1 ), the method of determining this being simple inspection of a truth-table for Ψ .The term 'Tarskian' in the ensuing theorem is chosen because A3 is the often so-called Law of Tarski with commuted antecedents.Def. £ For all Ψ , ψ is Tarskian iff there are valuations of ψ , say a and β, such that φ is F in α, T in β, and all arguments of Ψ that are T in β are T in a .THEOREM.A3 is independent in the system [Al-3, (<?)•} iff Ψ is not Tarskian.1 We are indebted to Professor Henkin for suggesting this problem.