0
$\begingroup$

Is there any smart way to check if certain statements are not provable in any of these proof systems?

Like for example the following task:

Prove or disprove the following statements:

  • $\vDash \exists x(\neg A(x) \lor \forall x A(x))$
  • $(\exists x A(x) \rightarrow \exists x B(x)) \vDash \forall x(A(x) \rightarrow B(x))$
$\endgroup$
2
  • $\begingroup$ If the firs one is $∃x¬A(x) ∨ ∀xA(x)$, it is obviously valid (LEM). If it is instead $∃x(¬A(x) ∨ ∀xA(x))$, an argument by case will do: either $∀xA(x)$ holds, or there is some $a$ for which $\lnot A(a)$. $\endgroup$
    – Mauro ALLEGRANZA
    Mar 16 at 7:50
  • 1
    $\begingroup$ Thank you! Yes I edited the question it is the case with parentheses. Do you have the idea how to perform a sequent calculus proof? The second statement should not be valid as each x that is A implies the existence of a possible different x that is B, does not mean that each x that is A is also B itself. $\endgroup$
    – jjbinks
    Mar 16 at 12:27

0

Reset to default

You must log in to answer this question.