1
$\begingroup$

Question: Does a semi-effective procedure for demonstrating that a formula is truth-functionally unsatisfiable count as a ``deduction method''?

Background: According to Warren Goldfarb, in his 1928 ``On Mathematical Logic'', Skolem

argues that if a formula [of first-order predicate logic] has a truth-functionally inconsistent expansion then it leads to a contradiction in his deduction-method. (Goldfarb, 1979, p. 363)

As Goldfarb acknowledges, the deductive system in question is not at all explicit. Skolem mentions a few inference rules involving quantifiers but does not give what we would call a formal system. The inference rules are not involved in Skolem's example of the method he would use to show a formula to be contradictory.

The method involves his level-by-level construction (same as in his 1923) of instances of the formula created by dropping the quantifiers and substituting integers for the variables. Each level adds new instances of the formula as the universal variables are taken to range over the integers introduced at the previous level. We then consider, at each level, all the possible truth assignments to atomic components that make the formula come out true ("solutions"). By the same argument used in 1923 to show that the sequence of solutions must converge after a finite number of steps (because there are finitely many solutions at each level), Skolem here argues that when the solutions converge a contradiction is revealed, provided the formula is not consistent. This contradiction is evidenced in the fact that there are no solutions of the next level that extend those of preceding levels - the formulas of this level are what Goldfarb calls a "truth-functionally inconsistent expansion" of the original. This concludes Skolem's method for showing a formula to be contradictory in a finite number of steps. But is it a "deduction"?

References:

GOLDFARB, WARREN D

[1979] Logic in the Twenties: The Nature of the Quantifier. Journal of Symbolic Logic, 44, pp. 351-368.

SKOLEM, THORALF

[1923] Einige Bemerkungen zur axiomatischen Begründung der Mengenlehre. Matematikerkongressen i Helsingfords den 4–7 Juli 1922, Den femte skandinaviska matematikerkongressen, Redogörelse . Helsinki: Akademiska Bokhandeln, 1923, pp. 217–232. English translation in van Heijenoort (ed.) [1967], pp. 290–231.

Improve this question
$\endgroup$
5
  • $\begingroup$ Why not? ------ $\endgroup$
    – Emil Jeřábek
    Commented Jul 10, 2020 at 5:50
  • $\begingroup$ @EmilJeřábek of course the truth table method can be used to establish that an argument is deductively valid, but the process described here of checking each level for truth-functional satisfiability does not fit the definition of a deduction as an argument going from premises to conclusion by validity-preserving inference rules. $\endgroup$
    – Mallik
    Commented Jul 10, 2020 at 21:31
  • 1
    $\begingroup$ The idea here is that checking propositional validity is so simple that it can be done by a single application of a rule. $\endgroup$
    – Emil Jeřábek
    Commented Jul 11, 2020 at 6:38
  • $\begingroup$ @EmilJeřábek I.e., for the propositional formulas at each level, the "deduction'' would begin by listing the atomic components, systematically constructing the truth table, and the rule would be "If at least one row of the table assigns "T" to the whole formula, write the formula; otherwise , write its negation." $\endgroup$
    – Mallik
    Commented Jul 11, 2020 at 16:44
  • $\begingroup$ Also, this would be a semantic procedure whereas Goldfarb has in mind something syntactic: 'Skolem seems to be groping for a more syntactical-but still not entirely formal-parsing of the notion "containing a contradiction", having in mind an informal deduction method.' (Goldfarb, 1979, p. 363) $\endgroup$
    – Mallik
    Commented Jul 11, 2020 at 18:10

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .