4
$\begingroup$

Hello all,

If you have a theorem $\vdash \alpha \rightarrow \beta$ and a theorem $\vdash \gamma$ then if $\alpha$ is a sub-expression of $\gamma$, and this sub-expression has an even number of negations within $\gamma$ (and it is not within a xor or boolean equality), then a new theorem can be obtained by replacing $\alpha$ with $\beta$ in $\vdash \gamma$.

Similar, if $\beta$ is a sub-expression of $\gamma$, and this has a odd number of negations, then a new theorem can be obtained by replacing $\beta$ with $\alpha$.

It is not so difficult to see that this is true, but has this rule a name? And is there any literature about it? If you introduce this rule, you can probably skip some axioms. Also, it is a more general form of modus pones.

The background of this question is, that one of my interests is how to do real mathematics in a formal logic. My opinion is that both sides should make steps to come closer to each other. Logicians should make logics that are more practical to use, and mathematicians should make proofs that are easier to formalize. I think above rule is quite natural for mathematicians, and can be verified by computer. At least when I am doing mathematics, I am well aware if a certain sub-expression is in a position that it can be weakened or strengthened. And I think that counts for all mathematicians.

With this rule you don't need the low-level proving with shifting assumptions in front of the $\vdash$ sign, to weaken or strengthen the sub-expression. This low-level shifting is a practice that in general can not be found in books of mathematics that do not deal with logic.

Regards,

Lucas

Improve this question
$\endgroup$

2 Answers 2

Reset to default
4
$\begingroup$

I don't know a name for the particular inference you indicate, but its feature that it operates "deeply" within the formulas at hand rather than at the root of their parse trees brings to mind current proof-theoretic work in deep inference. Perhaps check out Alessio Guglielmi's Deep Inference in One Minute; you might find that this blurb jibes with some of your motivation. Guglielmi's site in general is pretty comprehensive about this area, of which I know very little.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Thanks for the answer. I don't follow everything, but I read things that are somewhat similar to my own thoughts. $\endgroup$
    – Lucas K.
    Commented Dec 30, 2011 at 22:06
4
$\begingroup$

C.S. Peirce, in his calculus of Existential Graphs, had a rule very similar to this which he called "weakening" or "rules of insertion and erasure". The Wikipedia article is a little skimpy on this, but see the brief discussion on rules of inference (under Alpha), or see Peirce's Collected Papers (ed. Hartshorne and Weiss), vol. III and IV, section 4.505. (I am unable to locate the term "weakening" right now, but since Peirce had a tendency to write and rewrite again and again on his Existential Graphs, which he proudly considered his "chef d'oeuvre", I think with more effort I could locate it.)

Improve this answer
$\endgroup$
1
  • $\begingroup$ Thanks for the answer. Interesting that Peirce was already busy with these kind of things. $\endgroup$
    – Lucas K.
    Commented Dec 30, 2011 at 22:07

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .