Timeline for Hilbert style axiomatic proof or sequent Calculus?
Current License: CC BY-SA 3.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 26, 2014 at 11:29 | comment | added | Emil Jeřábek | Let me try again. A substitution is a mapping of formulas to formulas. In your example, it maps the formula CδpCδNpδq to the formula CCpCprCCNpCNprCqCqr. Its inner structure is not relevant here. The sequent substitution rule works by applying the same substitution to every formula in the sequent. I don’t know what’s not to understand here, but I can’t make it any more trivial than that. | |
| Apr 26, 2014 at 0:14 | comment | added | Doug Spoonwood | Substitution for δ (or "C" as you notated things), does not happen on formulas, because δ is not a formula. δ is a unary variable function (or functorial variable), but not a formula. If CδpCδNpδq is the starting point, then δ/C ' ' (substituting δ with C ' '), means we replace δp with C, then p, then p again since "p" is the argument for the first δ, δNp with CNpNp, and δq with Cqq. If we have CδpCδNpδq and substitute δ with C ' C ' r, then we obtain CCpCprCCNpCNprCqCqr. We can't say that we've substituted for $\delta$p since $\delta$p is not a variable, though δ is a variable. | |
| Apr 25, 2014 at 11:07 | comment | added | Emil Jeřábek | I can’t make heads or tails of your notation, but then again, I fail to see what the notation for substitutions has to do with anything. The substitution rule is not expressible in either sequent or Hilbert calculus, it is expressed in the metatheory where the calculi are being defined. A substitution is a particular operation $A\mapsto\sigma(A)$ on formulas. The substitution rule in Hilbert calculus is “from $A$ infer $\sigma(A)$”, and in sequent calculus it’s “from $A_1,\dots,A_n\Longrightarrow B_1,\dots,B_m$ infer $\sigma(A_1),\dots,\sigma(A_n)\Longrightarrow\sigma(B_1),\dots,\sigma(B_m)$”. | |
| Apr 24, 2014 at 16:22 | comment | added | Doug Spoonwood | I guess my question is, how is the substitution rule for δ, or "C" in your latest formula, expressible in sequent calculus? The notation I've seen writes something like $\delta$/C ' ' to indicate that $\delta$ should get substituted with C, then the argument belonging to $\delta$, and then the argument belonging to $\delta$ again. That is " ' " indicates that the argument that follows $\delta$ should go in that place. For instance, from the axiom C$\delta$pC$\delta$Np$\delta$q, $\delta$/ ' yields CpCNpq. $\delta$/C ' C N ' q yields CCpCNpqCCNpCNNpqCqCNqq. | |
| Apr 24, 2014 at 15:08 | comment | added | Emil Jeřábek | ... Or rather $\Longrightarrow C(A)\to(C(\neg A)\to C(B))$, as you seem to allow substitution for $\delta$ as well. Or just include the relevant substitution rule in the sequent calculus. | |
| Apr 24, 2014 at 11:42 | comment | added | Emil Jeřábek | I’m not familiar with your calculus, and I can’t say I fully understand the description, but I don’t see where is the problem. Just take the usual sequent calculus for classical logic augmented with $\Longrightarrow\delta(A)\to(\delta(\neg A)\to\delta(B))$ as an axiom. | |
| Apr 23, 2014 at 5:01 | comment | added | Doug Spoonwood | I thought this answer correct until I recalled that there exist Hilbert style calculi with functorial variables (not just propositional variables). For example, there's a Hilbert calculus for conditional [C]-negation[N] classical logic with just the axiom C$\delta$pC$\delta$Np$\delta$q under substitution (which applies to all variables) and detachment. How does one obtain the theorem CpCNpq or the theorem CC$\delta$ppCC$\delta$NpNpC$\delta$qq in a sequent calculus? | |
| Aug 21, 2013 at 13:27 | history | edited | Emil Jeřábek | CC BY-SA 3.0 |
added 970 characters in body
|
| Aug 21, 2013 at 12:54 | history | answered | Emil Jeřábek | CC BY-SA 3.0 |