Not all proofs use the law. Indeed, the law is not even usually one of the logical axioms. — TonesInDeepFreeze

They don't assert the Law of Contradiction explicitly, but they must assume that it is certain implicitly, otherwise it is not even possible to talk meaningfully, as Aristotle pointed out.

(1) Trivial. If the law is an axiom then it also provable by the rule of putting an axiom on a line. — TonesInDeepFreeze

Only if you assume that it is not also the case that the Law is not provable by the rule of putting an axiom on a line, which requires the Law of Contradiction and makes the “proof” circular. It certainly would not convince a LNC sceptic.

And the same applies for the rest of the “proofs”.

they must assume that it is certain implicitly — Amalac

They prove it as a theorem. Of course, our motivation for the system would include proving it as a theorem.

otherwise it is not even possible to talk meaningfully — Amalac

"Talk meaningfully" is a large and undefined rubric.

Only if you assume that it is not also the case that the Law is also not provable by the rule of putting an axiom on a line — Amalac

When I resolve the double negative, we get "It is the case that the law is provable by the rule of putting an axiom on a line", which is what I said in the first place.

the “proof” circular — Amalac

It is petitio principii. But ordinary logic allows it, otherwise you could never put a premise onto a line.

And the same applies for the rest of the “proofs”. — Amalac

First, I don't know why you put 'proofs' in what I surmise to be scare quotes.

Second, (1) is not petitio principii, unless you hold that proof from logical axioms is petitio principii. (2) Is basically an example of the principle of explosion itself closely related to LNC.

A word is not the same thing as that to which the word refers.

So if Amalac, in the following sentence, means “the word Amalac” then I am not Amalac.

If it means “the person writing this right now”, then I am Amalac.

The only way you can assert that I am both a person and a word is through either denying the Law of Contradiction, or through the fallacy of equivocation. — Amalac

Yeah, all of that. But that misses the point. There's a difference between "Amalac" and Amalac. But no difference between Amalac and Amalac.

They prove it as a theorem. Of course, our motivation for the system would include proving it as a theorem. — TonesInDeepFreeze

How do you know that (Edit: sorry, missed adding: “it's not the case that” here, I'm very tired from work) they also don't prove it as a theorem? By accepting the Law of Contradiction as an axiom? Then you are agreeing with me: It cannot be proven so it must be assumed as an axiom. By definition, axioms are accepted as true without proof. So the question is: Why should a LNC sceptic accept that axiom in the first place?

My point is that your proofs only work if someone accepts the Law as an axiom, if they don't, then your “proofs” are circular.

Talk meaningfully" is a large and undefined rubric. — TonesInDeepFreeze

Without assuming the Law as true without proof, for all I know you may have both asserted and denied everything you've said this far. That's what I mean.

Edit: sorry, got the quotes mixed up at first, since I'm writing from my phone's half broken screen I didn't notice.

But no difference between Amalac and Amalac. — Banno

Obviously not, but what exactly did you mean then? What point were you trying to get across here? :

Even as Amalac is both a word and you. — Banno

That noncontradiction is both the way the world is and a rule of language. It amounts to the same thing.

Ok, but like I said, Russell doesn't disagree and neither do I:

The belief in the law of contradiction is a belief about things, not only about thoughts.
— Russell

His “only” implies that he holds that the belief in the Law of Contradiction is both about thoughts and about things. — Amalac

OK, so what is at issue here?

Well, I thought you held that the Law of Contradiction was only a rule of language, but now you are saying that it does reflect how the world is.

What I don't understand is how that's consistent with this earlier statement of yours:

I think this because logic is about what we can say, and not about the way things are. — Banno

Well, I thought you held that the Law of Contradiction was only a rule of language, — Amalac

I do.

but now you are saying that it does reflect how the world is. — Amalac

...so does language.

Logic is about the rules of language. Language is about how the world is.

I'm not seeing a problem.

I think this because logic is about what we can say, and not about the way things are — Banno

The problem is that I don't agree with this statement: I think logic is about what we can say, but also about the way things are (in the sense in which Russell also holds this in that last statement of his that I quoted previously).

So how do you explain this disagreement when we seem to agree about the rest? That's what's got me a little puzzled, unless you changed your mind.

I think logic is about what we can say, but also about the way things are — Amalac

Yeah, alright, take it that I misspoke, and look a the following Sentence:

If we found a situation in which there was an apparent contradiction, what we would do is to re-think how we set out contradictions. — Banno

What I was aiming at is that logic is the handmaid of what is the case. One of the things we do with language is that when it doesn't seem to show us what is the case we change what we are saying.

DO you agree with that?

One of the problems here is that an essay is needed but I don't have time for that.

How do you know that they also don't prove it as a theorem? — Amalac

That's a very silly question. I don't know they don't prove it as a theorem, since it is not the case that they don't prove it as a theorem, and I can't know that which is not the case. Are you trolling me?

Or maybe you meant to type: How do you know that they also don't prove it is not a theorem?

And I answered that in a previous post. When we remove the double negative we get: How do you know that they prove is a theorem?

By accepting the Law of Contradiction as an axiom? — Amalac

We may agree with LNC and use LNC without LNC being an axiom.

By definition, axioms are accepted as true without proof. — Amalac

That's one notion. But another definition of 'axiom' is purely syntactical.

If your point is that LNC is endemic in reasoning, then I agree with you on that point. But that doesn't entail that LNC must be an axiom. (And I'm putting aside the matter of paraconsistent logic.)

It cannot be proven — Amalac

Now you're just reasserting a claim that I refuted.

Why should a LNC sceptic accept that axiom in the first place? — Amalac

It is fine to have it as a logical axiom, since it is logically true. Sceptics should learn that it is logically true.

My point is that your proofs only work if someone accepts the Law as an axiom — Amalac

That's false. The proofs can be mechanically audited whether the auditer knows of LNC as an axiom or not. Indeed, even for everyday reasoning, probably most people haven't even heard of LNC, especially the notion of it is an axiom. And that does not contradict that good reasoning (other than dialethistic) conforms to LNC and sometimes uses it - either as an explicit or implicit principle.

your proofs only work if someone accepts the Law as an axiom, if they don't, then your “proofs” are circular. — Amalac

You are reasserting a claim that I refuted.

Without assuming the Law as true without proof, for all I know you may have both asserted and denied everything you've said this far. — Amalac

It is possible for one to assert and deny a proposition. And it is even ubiquitous that people assert propositions that are inconsistent with other propositions. So probably what you mean is that it is not possible to be correct while both asserting and denying a proposition. Then your question seems to be how do we know that contradictions are not the case. But the question of how we know things is different from the question of what axioms we choose. We may know that a statement is true by reasoning from different axioms sets that each yield the statement as a theorem. It is not required that LNC be one of the axioms. If, as we ordinarily do, we require a system that is complete in the sense of proving all validities then it is only required that LNC at least be a theorem even if not an axiom.

Logic is about the rules of language. Language is about how the world is. — Banno

Logic is about entailment and inference. Logic concerns both syntax of language and meaning with language. Meaning includes denotation, which concerns individuals in the world. And meaning includes evaluation of truth of sentences, which concerns states-of-affairs in the world. ('the world' may be taken in such senses as the real world, possible worlds, fictional worlds, or mathematical worlds.) Generally speaking, logic doesn't say what is the case in worlds, but logic is not just rules of language unless included in those rules are the means by which we relate language to objects and what is the case in the world. Maybe said this way: Logic does not concern what is the case in the world, but rather logic does include concern of HOW language relates to what is the case in the world.

That's a very silly question. I don't know it, since it is not the case, and I can't know that which is not the case. Are you trolling me?

Or maybe you meant to type: How do you know that they also don't prove it is not a theorem? — TonesInDeepFreeze

Yes, that was my bad, I'm too tired from work, I wrote too quickly and forgot to add that other negation, I'll try writing more slowly now. (Also english is not my mother tongue so please have mercy on me).

That's one notion. But another definition of 'axiom' is purely syntactical. — TonesInDeepFreeze

Let's start here, what's this purely syntactical definition of “axiom” you speak of?

The proofs can be mechanically audited whether the auditer knows of LNC as an axiom or not. Indeed, even for everyday reasoning, probably most people haven't even heard of LNC, especially the notion of it is an axiom. And that does not contradict that good reasoning (other than dialethistic) conforms to LNC and sometimes uses it - either as an explicit or implicit principle. — TonesInDeepFreeze

But they must still accept it implicitly without proof (that's what I mean by “accept it as an axiom”). Of course we don't make all our inferences explicit, but we still implicitly infer many things, which require us to accept some propositions as true without proof, among which is the Law of Contradiction. As Aristotle said: It is utterly impossible to prove everything.

Someone who doubted that the Law of Contradiction was true, would not accept any proof that assumed, without proof, that the Law of Contradiction is true, he will demand that you prove it without having it as an axiom or assuming its truth in any way, since he won't accept circular arguments.

In one sense, it is trivially true that if you have the Law as an axiom, then you can prove that the Law is true. Likewise, if I have “God exists” as an axiom, I can prove that God exists.

Or if someone asked you to prove that 5=5, and you told them: “If you accept that A=A is true for any number you substitute for A, then it necessarily follows that 5=5” he may reply: “And why should I accept that A=A?”, and so it becomes clear that you can't convince him that 5=5. The same thing happens with the Law of Contradiction sceptic, you also can't convince them that the Law is true.

It is fine to have it as a logical axiom, since it is logically true. Sceptics should learn that it is logically true. — TonesInDeepFreeze

That's just an assertion, the LNC sceptic will demand a proof for it. They want to learn why it's true.

First, it is possible for one to assert and deny a proposition. And it is even ubiquitous that people assert propositions that are inconsistent with other propositions. So probably what you mean is that it is not possible to be correct while both asserting and denying a proposition. Then your question seems to be how do we know that contradictions are not the case. But the question of how we know things is different from the question of what axioms we choose. We may know that a proposition is true by reasoning from different axioms that each yield the proposition as a theorem. It is not required that LNC be one of the axioms. If, as we ordinarily do, we require a system that is complete in the sense of proving all validities then it is only required that LNC at least be a theorem even if not an axiom. — TonesInDeepFreeze

Could you please show me a proof of the Law of Contradiction that didn't have it as an axiom, and didn't assume that it is true,without proof, in any way?

What I was aiming at is that logic is the handmaid of what is the case. One of the things we do with language is that when it doesn't seem to show us what is the case we change what we are saying.

DO you agree with that? — Banno

Of course I do agree that we should make language fit what we know about reality and not the other way around. It may happen that, for example, we were wrong in thinking some object had a certain characteristic that we labeled X, because we made a wrong inference based on misleading or insufficient evidence, and later learned that that inference was wrong, and that the characteristics of that object were such that it didn’t fit in the definition of X, and in that case we would no longer say that it has that characteristic X.

But anyway, how does that lead to the claim that it is not possible to prove the existence of anything a priori, that is: that no analytic proposition can also be existential in its content? I suppose you may say that such a proposition would try to make reality fit into language rather than the other way around, but supposing God did exist, that would not be the case, we would in that case make language fit into reality.

forgot to add that other negation — Amalac

Yes, I mentioned it as a possibility. It was ungenerous of me to wonder whether you were trolling when Occam's razor would better suggest that you merely made a typo.

But again it boils down to:

When I resolve the double negative, we get "It is the case that the law is provable by the rule of putting an axiom on a line", which is what I said in the first place. — TonesInDeepFreeze

So I wonder why you still haven't recognize it, as I had already mentioned it twice.

what's this purely syntactical definition of “axiom” you speak of? — Amalac

A theory is a set of sentences closed under deduction.

(Some authors define a theory to be any set of sentences. And Enderton says a theory is a set of sentences closed under entailment, which is not syntactical. But they are equivalent with the completeness theorem, so, in that context, no harm done by saying 'closed under deduction' rather than 'closed under entailment'.)

A set of formulas S is an axiomatization of a theory T if and only if all members of T are provable from S. For a given axiomatization S of T, an axiom P is a member of S.

But they must still accept it implicitly without proof (that's what I mean by “accept it as an axiom”). — Amalac

That's a quite broad notion of axiom. It's not what 'axiom' usually means in a context such as formal logic, or as far as I know, even very much, if at all, in an informal discussion about reasoning.

It's not the case that sets of axioms are always independent, but independence of axioms is something we ordinarily desire.

As Aristotle said: It is utterly impossible to prove everything. — Amalac

Of course, I understand that in the everyday sense. But there is also a technical (though granted, pedantic) sense in which even axioms are provable. Also, for decidable theories, it is a decidable axiomatization where the set of axioms and the set of theorems are the same set.

Someone who doubted that the Law of Contradiction was true, would not accept any proof that assumed, without proof, that the Law of Contradiction is true — Amalac

That is incorrect. To accept a proof does not require accepting the truth of the premises. To accept a proof may be merely to audit that each step adheres to the rules of the proof system (the logic system). Thus, if the proof system is sound, then the assumption of the premises (no matter whether they are true of false) entails the conclusion.

it is trivially true that if you have the Law as an axiom, then you can prove that the Law is true. — Amalac

We can prove LNC is valid (even stronger than true). So we have the consequent of your hypothetical, so we don't need the antecedent. And we prove LNC is valid by proving that it is true in every model. That does not require proof in the logic system itself. However, its validity is entailed by proof in any logic system that that proves only validities (the soundness theorem).

if I have “God exists” as an axiom, I can prove that God exists. — Amalac

First, sentences of the form 'x exists' are not clear. One way to make them clear is with an existence predicate, but that is usually an advanced topic in predicate modal logic.

So I'll use this instead: G = "there exists a being that is omnipresent, omniscient, omnipotent, and omnibenevolent".

Then, yes, taking G as an axiom proves G as a theorem, but it doesn't prove that G is true. It only proves G is true if all the axioms used in the proof are true. So, since G is an axiom used in the proof, if it is false, then, though we have proved G, we have not proved that G is true.

It is fine to have it as a logical axiom, since it is logically true. Sceptics should learn that it is logically true.
— TonesInDeepFreeze

That's just an assertion, the LNC sceptic will demand a proof for it. They want to learn why it's true. — Amalac

No, it's not just an assertion. It's a theorem about propositional logic. And it is reducible, in a sense, to a theorem about Boolean algebra. And its proof is reducible to finitary operations, which are reducible to auditing the execution of an algorithm. So (heuristically speaking) we may say that at the root of the question is ability to audit the execution of an algorithm. Of course, it's hard to imagine such an ability in a person who was so delusional that they claimed to witness '0' and '1' written in the same space when only one of them was written in that space. But that is not the same as going all the way back up the chain of reductions I just described to say that LNC must be an axiom.

Could you please show me a proof of the Law of Contradiction that didn't have it as an axiom — Amalac

That might be tedious for me to type out, and if you are not familiar with proof calculi for propositional logic, then it wouldn't be of much use to you.

I recommend 'Logic: Techniques Of Formal Reasoning' by Kalish, Montague, and Mar. Within about a chapter you could assign yourself the easy exercise of deriving LNC in the natural deduction system there.

That is incorrect. To accept a proof does not require accepting the truth of the premises. — TonesInDeepFreeze

Oh, well if that's what you meant then obviously, if one of the premises is the Law of Contradiction or assumes the Law of Contradiction, the sceptic can just grant the validity of the proof while denying both that premise and the conclusion. He would say: “yes, obviously if the Law of Contradiction is true, then the Law of Contradiction is true, but I'm questioning the claim that the Law of Contradiction is true, not the implication”.

It only proves G is true if all the axioms used in the proof are true. So, since G is an axiom used in the proof, if it is false, then, though we have proved G, we have not proved that G is true. — TonesInDeepFreeze

Right, so the same thing that you say about G, one could say about the LNC: we have proved the LNC, but we have not proved that the LNC is true. The sceptic wants a proof that the LNC is true, that's the proof I was refering to.

However, it seems you say that unlike for G's truth, there actually is a proof that the LNC is true (not merely a proof of the LNC), is that right? It seems it's the one you are refering to here:

No, it's not just an assertion. It's a theorem about propositional logic. And it is reducible, in a sense, to a theorem about Boolean algebra. And its proof is reducible to finitary operations, which are reducible to auditing the execution of an algorithm. So (heuristically speaking) we may say that at the root of the question is ability to audit the execution of an algorithm. Of course, it's hard to imagine such an ability in a person who was so delusional that they claimed to witness '0' and '1' written in the same space when only one of them was written in that space. But that is not the same as going all the way back up the chain of reductions I just described to say that LNC must be an axiom. — TonesInDeepFreeze

I recommend 'Logic: Techniques Of Formal Reasoning' by Kalish, Montague, and Mar. Within about a chapter you could assign yourself the easy exercise of deriving LNC in the natural deduction system there. — TonesInDeepFreeze

Thanks for the recommendation, I'll read when I have the time (if I can find the book, that is).

it's the one you are refering to here: — Amalac

Yes, it's the proof of a theorem about propositional logic. And we prove not just that LNC is true in a particular model but moreover that it is true in all models (i.e. that it is a validity).

I realized that a natural deduction proof of LNC is also trivial. This one has different notation, but it is essentially the same as in Kalish, Montague, and Mar and other common systems:

1. P & ~P assumption {1}
2. P simplification {1}
3. ~P simplification {1}
4. ~(P & ~P) RAA [1, 2, 3]

The ease of getting LNC from RAA illustrates the closeness between RAA and LNC. So we are tempted to think LNC and RAA are conceptually "the same". But from LNC to RAA is only one direction. The other direction is from LNC to RAA. So we ask how easy is to get to RAA from LNC. That depends on the particular Hilbert style system we use. A Hilbert style system is a combination of axioms and rules, and RAA in natural deduction systems, unlike LNC, is a rule, not a theorem nor an axiom. So we would be deriving a rule from a combination of axioms and rules.

So there are two tasks: (1) Derive LNC from a Hilbert style system that does not have LNC as an axiom, and (2) Devise a system, without RAA, in which LNC is an axiom, and derive RAA.

Task (1):

A common Hilbert style system (call it 'H1') is given by:

Capital letters are meta-variables ranging over formulas.

Axioms:

A1. P -> (Q -> P)
A2. (P -> (Q -> R)) -> ((P -> Q) -> (P -> R))
A3. (~P -> ~Q) -> (P -> Q)

Rules:

R1. Any axiom can be put on a new line.

R2. If P is on a line and also (P -> Q) is on a line, then Q may be put on a new line.

Definition:

D1. P & Q stands for ~(P -> ~Q).

[end description of H1]

From D1, LNC is:

~(P -> ~P)

And that is what we need to derive. To reduce tedium, the natural suggestion is to first derive RAA as a rule, then apply RAA as previously in this post. Deriving RAA as a rule is a lot of steps, but it is fairly straightforward to do and I think it's fairly common in textbooks. So, I'm not going to type it here.

But since LNC is couched with & and ~, an even clearer approach would be to take & and ~ as the primitives. Then put the axioms in those terms for system H2:

D2. P -> Q stands for ~(P & ~Q)

So A1 - A3 become:

A4. ~(P & ~~(Q & ~P))

A5. ~(P & ~~(Q & ~R)) -> ~(~(P & ~Q) & ~~(P & ~R))

A6. ~(~(~P & ~~Q) & ~~(P & ~Q))

Take an instance of A4:

~(P & ~~(P & ~P))

Eliminate double negation:

~(P & (P & ~P))

Apply associativity:

~((P & P) & ~P)

Apply idempotency:

~(P & ~P)

So, lo and behold, there's LNC.

So we might be tempted to say that H2 itself is a Hilbert style system with LNC as a "subschema" of one of the axiom schemas; that LNC was there all the time, hidden but implicit. Ah, but not so fast there, pardner. First we have to derive rules for double negation, associativity, and idempotency.

A more elegant argument is simply to point to the completeness theorem for H2:

H2 is entailment complete.
LNC is a validity.
Therefore, LNC is a theorem of H2.

But to be convinced of the conclusion, we need to witness the proof that H2 is entailment complete and witness the proof that LNC is a validity.

Task (2)

Offhand, I don't know of a Hilbert style system that has LNC as an axiom. We could add LNC to the axioms of H2, but that would result in system with a non-independent axiom set. That's logically permissible, but it is inelegant and it reduces the challenge, which might not want to do. So the interesting question is to find an independent and entailment complete set of axioms that includes LNC.

Lemon gives this brief natural derivation:

(1) P & ~P Assumption
(2) ~(P & ~P) 1, 1, RAA

There's the predicate version to consider, too:

⊢(x) ~( F(x) & ~F(x) )

And since modal logic presumes the theorems of predicate and propositional logic as necessary,

▢ ~(P & ~P)
▢ (x) ~( F(x) & ~F(x) )

We might go the other way, and take LNC as a given in order to derive RAA.

take LNC as a given in order to derive RAA — Banno

Right, that was my Task (2). But I mentioned considerations about in my last paragraph.

The natural way to do it is first to derive the deduction theorem:

Where G is a set of formulas and p and q are formulas, then:

If G u {p} |- q, G |- p -> q

Then make that a derived rule. Then deriving RAA as a rule is only a few steps away.

It also occurred to me that someone who thinks LNC is always primary could argue:

Even given the explanations about deducibility, LNC entails (entailment is semantic) a subset of the instances of Axiom A4 and Axiom A4 entails LNC, so they are logically equivalent. That's true, but it doesn't advance any argument, because trivially all the validities are logically equivalent anyway.

OK.

This line of thinking came about as a result of @Bartricks's claim that LNC is true but contingent. Now he doesn't have a consistent leg to stand on, but he might be understood as denying

▢ ~(P & ~P),
or
▢ (x) ~( F(x) & ~F(x) )
or both. (edit: ah - the second is just an instance of the first... )

It should be apparent that it is inconsistent to deny these and yet assert ~(P & ~P).

In his case there seems to be a failure to understand that ▢ P ≡ ~♢~P. I've never seen a denial of this elsewhere.

'E!' is being used as a 1-place predicate symbol. — TonesInDeepFreeze

This is how "...exists" must be used in the ontological argument.

So one version fo my OP would be to ask if (x) ▢(E!(x)) - if there is some being that exists in all possible worlds.

But it seems clear from the discussion that E!(x) must mean that x is in the domain; and since the domain is decided more of less by fiat, in effect prior to any deductions.

Hence I don't see that E!(a) can be the result of a deduction.

Going back to your first post:

In S4 or S5, or a derivative therefrom, can an individual exist in every possible world without contradiction? — Banno

I don't know what you mean by that. There is mention of systems and contradiction, which is syntactic, and mention of worlds, which is semantic. It's not clear to me what relationship between them you are asking about. Also, 'possible world' is relative to a given world and the accessibility relation, so what do yo mean by 'in every possible world' without reference a single world as the "base" from which other worlds are accessible to it? Or maybe you just mean just "in all worlds", so that we could delete the word 'possible'?

But more fundamentally, S4 and S5 are not predicate modal logics. So there is no semantics about individuals.

I'm interested in your question, but I wonder whether you might reformulate it.

Bartricks's claim that LNC is true but contingent — Banno

Would you please link to it?

'E!' is being used as a 1-place predicate symbol.
— TonesInDeepFreeze — Banno

Since that post, I am reading to find more about the existence predicate (that I would call just 'E' and not 'E!' as others have), but I haven't yet caught up to seeing exactly how it works.

one version fo my OP would be to ask if (x) ▢(E!(x)) - if there is some being that exists in all possible worlds. — Banno

I'll rewrite that in text only ('A' for universal quantifier, 'N' for 'necessarily', 'X' for the existence predicate.

Ay N Xy

But what do you mean by "if"? Are you asking whether it's a theorem of some given system? (That system wouldn't be S4 or S5, since those are merely propositional logic systems, or do you mean a quantified version of S4 or S5?) Or are you asking whether there are models in which the formula is true?

Why not this trivial model?

w has domain = {0}
W = {w}
R = {<w w>}
f = {'c' 0}

Oh, formulating the question was as much a part of this thread as the question itself.

The thread was https://thephilosophyforum.com/discussion/11355/necessity-and-god/p1 . This thread was an attempt to formalise to some degree the intuition in the OP of that thread.

That intuition is that for any individual, one can give consideration to what the world would be like without that individual.

But if there is a necessary being, then it would not be possible to give consideration to a wordl without that being.

Sorting out this incompatibility has helped keep me from doing some paving in the front garden for a few days now.

The discussion with Bart is in that thread, form about here: https://thephilosophyforum.com/discussion/comment/564170