Natalie Clarius

Yeah, I'm with PW_246 here in that free logic is not what "classical logic" is typically understood to mean, but of course what you meant is true - perhaps one could have said it isn't valid even in "non-constructive" logics as long as they don't assume a non-empty universe, and everyone is happy.

Classical logic does always assume that something exists though.

@rooke_of_math For the tableau method, especially if you're interested in the systematic development: Raymond Smullyan (1968) First-order logic. To learn natural deduction you could check out forallx.openlogicproject.org/forallxyyc.pdf.

Sure, go ahead. (As I said, I do think one can view tableaus as more semantic, in a way, than other proof methods; the distinction "syntactic"/"semantic" is common but not very precise in various respects.)

... I would like to end this discussion here and wait for the OP to decide which of our answers (if not both) is useful to them.

I know very well what the tableau calculus is, and I know for sure that I didn't use it. A tableau does the argumentation mechanically, I did not, that's precisely why my answer is not about some algorithmic decision procedure, and that dosen't make me wrong in any way. An informal proof is a proof, period. None of our answers is wrong, the only thing to argue about is whether this is the answer that OP is looking for, and since nothing in their post clearly indicates that they is only interested in one of them or is even aware of the distinction, ...

And I absolutely did not "go on to basically use ST", my answer has nothing to do with tableaus apart from the fact that I mentioned one could achieve the same results with it. The fact that the tableau calculus exists and is sound and complete doesn't make a purely argument-based proof wrong at all.

Yes, and this proof can be carried out either informally or formally. I gave the first and you gave the second; both are kinds of proofs, and hence also why I clarified in my answer what is meant by "formal" and "informal" proof.

One could argue about how directly "semantic" the truth table method and the tableau method are as opposed to e.g. natural deduction, but the tableau method definitely can be classified as a calculus in the sense that it is a fully formalized system with a fixed set of rules operating purely on symbols without making explicit reference to structures. Yes, one neat thing about tableaus is that we can read off counter models from open branches, and of course the truth conditions are reflected in the rules, that's why it's sound, but that doesn't make it a purely semantic/non-syntactic method.

OP nowhere asked for an algorithmic decision procedure, they asked for an example of a proof.

Sure, go ahead. (As I said, I do think one can view tableaus as more semantic, in a way, than other proof methods; the distinction "syntactic"/"semantic" is common but not very precise in various respects.)

I know very well what the tableau calculus is, and I know for sure that I didn't use it. A tableau does the argumentation mechanically, I did not, that's precisely why my answer is not about some algorithmic decision procedure, and that dosen't make me wrong in any way. An informal proof is a proof, period. None of our answers is wrong, the only thing to argue about is whether this is the answer that OP is looking for, and since nothing in their post clearly indicates that they is only interested in one of them or is even aware of the distinction, ...

... I would like to end this discussion here and wait for the OP to decide which of our answers (if not both) is useful to them.

Yes, and this proof can be carried out either informally or formally. I gave the first and you gave the second; both are kinds of proofs, and hence also why I clarified in my answer what is meant by "formal" and "informal" proof.

And I absolutely did not "go on to basically use ST", my answer has nothing to do with tableaus apart from the fact that I mentioned one could achieve the same results with it. The fact that the tableau calculus exists and is sound and complete doesn't make a purely argument-based proof wrong at all.

OP nowhere asked for an algorithmic decision procedure, they asked for an example of a proof.

One could argue about how directly "semantic" the truth table method and the tableau method are as opposed to e.g. natural deduction, but the tableau method definitely can be classified as a calculus in the sense that it is a fully formalized system with a fixed set of rules operating purely on symbols without making explicit reference to structures. Yes, one neat thing about tableaus is that we can read off counter models from open branches, and of course the truth conditions are reflected in the rules, that's why it's sound, but that doesn't make it a purely semantic/non-syntactic method.

"but since its conclusion is a tautology in this case, does that fit the definition of validity anyway?" Yes, exactly. That's why it is not invalid.

But I think the matter about discharging assumptions and having multiple occurrences makes more sense and is easier to see in the tree-style format as presented in van Dalen, where cancelled assumptions just get bracketed and marked with an index.

If you wanted to make it dependet on one of the Ps but not the other, you would have to do a nested subproof with two of the P assumptions and place the conclusion such that it is outside the inner P subproof but still inside the first one -- something like this: pastebin.com/2U8RGnsS Since the conclusion is the conclusion is inside the outer two vertical lines headed by Q and P respectively, that's the assumptions on which it depends.

In Fitch-style notation discharging assumptions corresponds to leaving a subproof and going one vertical indentaiton line back, so by placing the conclusion P -> Q on the level of the outer proof, rather than in the subproofs with assumptions P, the only open assumption at that point is Q.

Note also that you are allowed to write whatever additional premises left of the $\vdash$ even if they don't occur as open assumptions in your derivation: The definition of $\vdash$ is that there is a tree whose open assumptions are a subset of the premises, given your derivation of proving P -> Q from Q, you are allowed to write not only Q |- P -> Q, but also e.g. R, Q |- P -> Q.

Re. your last comment: Yes, that's correct.

If you have 5 occurrences of the assumption, you can discharge 0, 1, 2, 3, 4, or 5 of these occurrences. If you have 0 occurrences of the assumption, you can apply the rule anyway.

No, leaving some or all assumptions undischarged is explicitly a correct rule application. You can and typically want to cancel dischargeable assumptions, but you don't have to. That liberty is part of how cancellation is defined.

Oh, you found that exact passage. Should have finished reading all your comments before starting to talk agian.

It is explained on p. 34: "W.r.t. the cancellation of hypotheses, we note that one does not necessarily cancel all occurrences of such a proposition \psi. [...] Furthermore, one may apply (-> I) if there is no hypothesis available for cancellation."

This holds for all rules that allow to discharge assumptions: You can either discharge all occurrences, leave all of them open, discharge some while keeping others open (talking about occurrences because it could be that the assumption was used multiple times in the derivation of the conclusion), or have no occurrence of the assumption at all. Other rules that allow to discharge assumptions are $\neg I$ (discharging the unnegated assumption), $\bot$ (discharging the negated assumption) and $\lor E$ (discharging the two disjunctions).

That this is generally allowed is not obvious from the notation in the rule schemata themselves and probably was mentioned in the text when introducing the ND notation and explaining the discharging of assumptions.

The point of this exercise (I think) is to have understood that $\to I$ (and other rules that allow to discharge assumptions) may be applied without discharging (all) occurrences of the assumptions, or (like here) without the assumption even present in the derivation at all.

You already used this correctly in your proof. The rule ($\to I$) $\quad [\psi]^i \cdots \phi - \psi \to \phi\quad $ states that the antecedent $\psi$ to be introduced is an assumption from which $\phi$ was derived and which may be [discharged]${}^1$ when applying the rule. But in your proof, the assumption $\psi$ does not exist in the derivation of $\phi$, and we are allowed to $\to$-introduce it anyway: Dischargeable assumptions need not be actually present in the derivation.

The other half of the issue is that existing occurrences of dischargeable assumptions need not actually be discharged: $\psi \cdots \phi - \psi \to \phi$, yielding $\psi \vdash \psi \to \phi$ (instead of $\vdash \psi \to \phi$) would also be a correct application of the $(\to I)$ rule.

Correct; well done!

The reason why the semantic and syntactic definitions can be used interchangeably to some degree is because they are equivalent: The formulas such that $\vDash P$ are exactly the same formulas such that $\vdash P$: The syntactic proof system is sound and complete w.r.t. the semantics. (But this can not be taken for granted and has to been shown (complicated).)

And you can forget about the role of "classical" for the moment; everything that's done in the book (at least up to this point) is classical logic.

But this distinction is a different matter from the one between propositional logic and predicate logic: The book introduces propositional logic from the semantic side and predicate logic from the syntactic side, but as elaborated in the next paragraph on p. 30, one can also define a proof system for propositional logic and semantic clauses for predicate logic.

I now read through p. 30 and admit it is formulated a bit confusingly. The analogy that is made is between semantics ($\vDash$, truth tables) and syntax ($\vdash$, proof systems). The analogy can be made because $\vDash$ and $\vdash$ do in fact induce the same relations -- the same formulas that are tautological are provable -- though their definitions are different.

Both the propositional logic and the predicate logic, and both the truth conditions and the proof system you got to know until know, are for classical logic.

The distinction is between truth conditions/interpretations/models (via truth tables or clauses on truth conditions in a structure) on the one hand, and formal systems (which only have axioms and rules of inferences, and do not explicitly talk about interpretations) on the other hand.

Both propositional and predicate logic have a truth-conditional semantics and proof systems. It is not true that one is based only on truth conditions and the other is based only on the notion of proof; both are defineable for both logics.. There are proof systems for propositional logic, and there is a truth-conditional semantics for predicate logic.

The semantics for the connectives in classical prediate logic is the same as those for the connectives in classical propositional logic; the truth table for $\to$ is the same in classical propositional logic and classical predicate logic. Predicate logic is a more powerful extension of propositoinal logic, but with the same basic laws.

There is classical propositional logic (with propositional variables p, q, r, ... and truth tables), and classical predicate logic (with predicates P(x), Q(y,z), and quantifiers $\forall, \exists$).