With the following (false) argument, one could claim that PL1 is decidable: We take a complete proof calculus for PL1. W
Posted: Fri Apr 29, 2022 6:37 am
With the following (false) argument, one could claim that PL1 is decidable:
We take a complete proof calculus for PL1. With it we can find a proof for any true formula in finite time. For every other formula / I proceed as follows: I apply the calculus to ¬/ and show that ¬/ is true. Thus / is false. Thus I can prove or refute every formula in PL1. Find the mistake in the argument and change it so it becomes correct.
(b) Construct a decision process for the set of true and unsatisfiable formulas in PL1.
We take a complete proof calculus for PL1. With it we can find a proof for any true formula in finite time. For every other formula / I proceed as follows: I apply the calculus to ¬/ and show that ¬/ is true. Thus / is false. Thus I can prove or refute every formula in PL1. Find the mistake in the argument and change it so it becomes correct.
(b) Construct a decision process for the set of true and unsatisfiable formulas in PL1.