4

  1. Monotonicity is defined as the implication: M $\vdash$ A $\to$ M $ \cup$ N $\vdash$ A. It depends on the calculus if it is true or not. Correct?

  2. But the following semantic version is always true in classical logic: M $\vDash$ A $\to$ M $ \cup$ N $\vDash$ A. Correct?

  3. What is the name of the property of 2. because it seems to me that monotonicity is only used as a (syntactical) proof concept as in 1.

  4. How do you prove 1. for a proof system P since you cannot prove it in P itself because it is metalanguage? How does it work conceptually?

  5. How do you prove 2.?

  • It is weird to put implication between two turnstyles, I am guessing it means entailment. Is $M\cup N$ supposed to be $M∧N$ (concatenation of premises)? The way to prove it is to show how to construct a proof of the latter from a proof of the former. Most proof systems either include conjunction elimination as a primitive rule, or it is derivable from them, so 1 follows by the obvious construction. 2 is trivial, in all models where $M\cup N$ hold $M$ holds in particular, and then so does $A$. – Conifold Sep 08 '21 at 06:25
  • No. (M $\vdash$ A) $\to$ (M $ \cup$ N $\vdash$ A) is not the same as (M $\vdash$ A) $\vdash $ (M $ \cup$ N $\vdash$ A). It‘s just a statement that says: if you can prove A out of B $\in$ M then you can prove A out of B,C $\in$ M $\cup$ N. You cannot prove that in a normal proof system, you look for a meta-proof system. For instance you cannot prove it in the calculus of natural deduction because in this a proof has only one „$\vdash$„ symbol. You would need to construct a meta-proof system of natural deduction that enables you to work with two $\vdash$-symbols. –  Sep 08 '21 at 18:56
  • Of course this can be done. –  Sep 08 '21 at 18:58
  • You do not really need a special meta-proof system and symbols, vernacular is enough, but reasoning about symbolic proofs is trivial to formalize. "If you can prove A out of B ∈ M then you can prove A out of B,C ∈ M ∪ N" is not what implication means, it is exactly proof theoretic entailment. – Conifold Sep 08 '21 at 19:44
  • See this is what I do not understand. "If you can prove A out of B ∈ M then you can prove A out of B,C ∈ M ∪ N" is not what implication means“. But that statement IS an implication, is it not? So my definition of monotonicity is an implication and it is this implication that has to be proven, right? On the other side, entailment is just a process of proving things, while the implication is its result in a nutshell. Correct? –  Sep 09 '21 at 01:09
  • "In proof theory, a structural rule is an inference rule that does not refer to any logical connective, but instead operates on the judgment or sequents directly. Structural rules often mimic intended meta-theoretic properties of the logic. Logics that deny one or more of the structural rules are classified as substructural logics (such as linear logic, relevance logic, etc)." See reference here. Btw, you seem illogical here since you already accepted an answer while still confused?... – cinch Sep 09 '21 at 02:11
  • Colloquial meaning of "implication" is not very useful here, it mostly ignores differences between implication, inference, entailment, etc. Implication in logic is a connective that produces a formula, in this case a meta-formula. It does not make sense outside of a specific proof calculus, which you do not have. Your claim is instead semantic statement about the "process", about what can be done with proofs, see Proof-Theoretic Semantics. The two are related only on the assumption that your calculus satisfies deduction theorem. – Conifold Sep 09 '21 at 04:01

2 Answers2

1
  1. Monotonicity is defined as the implication: M $\vdash$ A $\to$ M $ \cup$ N $\vdash$ A. It depends on the calculus if it is true or not. Correct?

Yes, but it will hold for any calculus that is complete for classical logic.

  1. But the following semantic version is always true in classical logic: M $\vDash$ A $\to$ M $ \cup$ N $\vDash$ A. Correct?

Yes.

  1. What is the name of the property of 2. because it seems to me that monotonicity is only used as a (syntactical) proof concept as in 1.

If anything I'd say that monotonicity is a more semantic notion, and a term that is more closely associated with proof systems is weakening.

  1. How do you prove 1. for a proof system P since you cannot prove it in P itself because it is metalanguage? How does it work conceptually?

Yes, you will have to make a proof arguing about the calculus, though usually it's pretty much a direct consequence of how the proof system is set up. E.g. in natural deduction, $M \vdash A$ is defined to hold iff there exists a derivation with all the right rule applications ending in $A$ and the open assumptions a subset of $M$. Now of course every subset of $M$ is also a subset of $M \cup N$, and so the same derivation serves as a proof of $M \cup N \vdash A$.

  1. How do you prove 2.?

See Mauro Allegranza's answer: Every model of $M \cup N$ is also a model of $M$ and therefore, by assumption, a model of $A$, hence $M \cup N \vDash A$.

Natalie Clarius
  • 10,530
  • Here‘s my problem. I define monotonicity to be M $\vdash$ A $\to$ M $ \cup$ N $\vdash$ A. So this is the statement I have to prove. But in natural deduction I cannot prove it because „M $\vdash$ A“ and „M $\cup$ N“ are not a wff there. So we‘d need to introduce some further natural deduction system where both become wff‘s. Then it‘s simple (I spare the proof here). Is this basically how it works? –  Sep 09 '21 at 01:21
  • Not sure what you mean. They are not formulas, but meta statements, that's why you use a proof in the meta language and not within the deduction system. – Natalie Clarius Sep 09 '21 at 09:24
  • What proof system in meta-language? Basically it will be just some proof system enhanced by new rules that make the meta-language statement a wff there, isn‘t it? Then my monotonicity staement becomes just an implication there which we need to prove. –  Sep 10 '21 at 03:10
  • No. Meta language precisely means not any formal system. Meta language means English. – Natalie Clarius Sep 10 '21 at 09:37
0

See Monotonicity of entailment:

How do you prove 2.?

You can prove it directly using the definition of logical consequence:

if formula $\varphi$ follows from the set $\Gamma$ of premises (in symbols: $\Gamma \vDash \varphi$), then every model of $\Gamma \cup \{ \alpha \}$ will be also a model of $\Gamma$, and thus it will satisfy $\varphi$.

Mauro ALLEGRANZA
  • 94,169