Truth, falsehood, and contingency in first-order predicate calculus.
Charles G. Morgan · Notre Dame Journal of Formal Logic · 1973
In this paper it is indicated how the results obtained in [l] may be extended to languages with the syntax of first-order predicate calculus.An additional important result is demonstrated to the effect that there can be no proof procedure for the set of logically contingent expressions.The proof of this latter result depends on the undecidability of the predicate calculus, and hence it does not apply to the sentential calculus.At this time the existence of a proof procedure for the logical contingencies of sentential calculus is an open question. Preliminaries.Consider a formal language L with the following symbols:Predicates: P, P ι , P 2 , . . .(of varying degree) Individual constants: a, cii, a 2 , . . .Individual variables: x, x l9 x 2 , . . .Sentential connectives: & -"and," v--"or," -"not" Punctuation: ). and ( Quantifiers: (x) -"for every x," ( : x) -"for some x" I will assume the standard definitions of "well-formed expression of L ," and "atomic expression of Z./' The meta-symbols E, Eχ,E 2 , ---will be used to refer to well-formed expressions of the language.I will presuppose the standard semantical theory of such languages, including the semantical definitions of "logically true" (LT), "logically false" (LF), "logically contingent" (LC), and "logically equivalent" (LE).Let some axiomatic system PCT for L be given (the results in this paper apply to natural deduction systems as a special case).PCT will have axioms TA λ , TA 2 , . . ., TA n and a set of transformation rules (proof rules) TR 1 , TR 2 TR m .Let λ be a set of expressions of L, perhaps empty.If there is a proof of expression E from λ in the system PCT, I will write λ \-( E. I will assume that PCT has the following properties: