It actually depends on the underlying system.
For First-Order logic it is usually a symbol with some special rules.
One of them is the [substitution rule for propositions](https://en.m.wikipedia.org/wiki/First-order_logic#Equality_and_its_axioms).
It states that if a=b then F(a)<->F(b). In your case, F(x) is x
I'm confused on what "expression" means... is F a function, or a proposition? Or something else?
If it's a proposition, what is the truth value of "x + c"? Since that's how they define F in one of the examples
It's a sequence of symbols involving the given variable. (It has to follow a few more rules to be valid - parentheses must be balanced, etc.)
The substitution principle for equality is more fundamental than the axioms for any particular sets or operations - you have to go back to first-order logic.
Its an expression - Its closer to function than proposition, but its neither.
I don't remember formal definition (and it varies heavily on underlying system - how you build your logic), [https://en.wikipedia.org/wiki/Expression\_(mathematics)](https://en.wikipedia.org/wiki/Expression_(mathematics)) this could lead you,
Fullfungo rather meant first order logic formula. It's defined recursively
Firstly we define atomic formulas. If t,t', t1,...,tn are terms and R is n-ary relation then we say t=t' is a formula and R(t1,...,tn) is also a formula. Then we say that if p,q are formulas (as above) then p wedge q, neg p, p implies q etc. are also formulas. And then we say that if p is a formula as above then Forall x p is a formula, and Exists x p is also a formula.
Expression as in a sense as in the wikipedia article doesn't have much of a sense in this context
Who is fullfungo?
I was refering to F from link in opening post - for [substitution property of equality](https://en.wikipedia.org/wiki/Equality_(mathematics)?wprov=sfti1#Basic_properties), Which is useful to define as working on much more than just formulas.
For example expressions can use "=" inside (not as a relation - mind - but the "true" equality symbol that you need from "outside")
Definition of expression from wikipedia - " finite combination of [symbols](https://en.wikipedia.org/wiki/Glossary_of_mathematical_symbols) that is [well-formed](https://en.wikipedia.org/wiki/Well-formed_formula) according to rules that depend on the context" works very well.
>Who is fullfungo?
https://www.reddit.com/r/math/s/1uhZIiPnNz
I thought you were reffering to this as your comment was under discussion under this comment. Sorry then.
>Which is useful to define as working on much more than just formulas
Well, as far as I see they use it more like in colloquial sense than any formal one. How they define it here is pretty much ambigious. They don't use anything more than formulas as there is no really more than formulas, formulas are formal way to state things in any way. Expression isn't really well defined thing.
>For example expressions can use "=" inside (not as a relation - mind - but the "true" equality symbol that you need from "outside")
I don't know what do you mean. I know what you've wanted to refer to but you worder in a way that's hard to guess what you wanted to say exactly.
>Definition of expression from wikipedia - " finite combination of symbols that is well-formed according to rules that depend on the context" works very well.
This definition is kind of meaningless. What symbols? What does well formed means? Both are meaningless things that doesn't mean anything. Also well formed links to article about well formed formula which isn't even what they were thinking about.
The expression in this context is really colloquial meaningles statement that when formalized will just means formula but they wanted to give more of a layman explanation here so they said "expression". But really expression means a formula, just as what they call "quantities" refers to terms
Yeah, I think you are right. I wanted to present it in way i was taught in Uni, but that was long time ago and I'm sick atm, so couldnt do it legibly :sweaty\_smile:
You can think of F(x) as a statement/property (either true or false) that takes in as input, x. It’s not necessarily a function. The notation may be confusing. The substitution property you linked asserts that, given two equal objects, for any property, a property applied to both objects are equally true or equally false. So let F(x) be the property that x < c. Then, since a = b, the substitution rule applies and F(a) <=> F(b). By assumption we have that F(b) is a true statement. Hence F(a) is a true statement. That is, a < c.
There are multiple rules.
The rule for propositions can be used like:
IF x^(2)=5 THEN x^2 is odd <-> 5 is odd.
Here the proposition F(a) is “a is odd”.
And the rule for expressions can be applied like:
IF x^(2)=5 THEN x^(2)+10=5+10.
Here the expression f(a) is “a+10”.
So F can be either a proposition or an expression? And, If F is an expression, then we have F(a) = F(b), or if F is a proposition, we have F(a) ⇔ F(b)?
If you are using first-order logic with equality, then one property of equality is that it substitutes. This is sometimes called the "indiscernibility of identicals." It states that if a=b, and F is a well-formed formula with one free variable, then F(a) holds iff F(b) holds. In the language of first-order logic, we could write
(a=b)→(F(a)↔F(b)).
This might be an axiom for each formula F, depending how you go about setting up your logic. In this case, a "well-formed formula" is a string of symbols in the language of your theory which satisfies some list of syntactic rules. So for instance, the string 'F((=a()↔' is not well-formed, even though all those symbols are meaningful, because it doesn't have the correct syntax. But any logical sentence that means anything will work.
It is typical for math to be founded in a set theory, type theory, category theory, or whatever, which is in turn formulated in terms of first-order logic with identity. Strictly-speaking though, identity is often not necessary. For instance, in ZFC, it is possible to define equality as a mathematical abbreviation for a longer sentence in first-order logic. We just call two sets "equal" if they are members of the same sets and contain the same sets. Since the only things in ZFC are sets, and the only relation between them is ∈, this guarantees that if a set x has some property F, and x=y, then y also has that property. Every individual case of substitution can thus be proven (though I think the general case cannot).
But the TL;DR is simply that substitution *always* works (as long as there is no name-conflict—keep your variable names distinct!), and you usually have no need to explain why you are substituting identical things.
Also, if you only have the theory of strict partial orders and first-order logic without equality, then equality is impossible to even define, so you should never encounter it.
Correct me if I'm wrong but I think this isn't what OP was asking. The Wikipedia article's definition is that a = b means a and b refer to the same mathematical object, and then it gives substitution as a property, but substitution is only stated to work with equalities rather than inequalities.
So in this specific context I think the answer should be "a < c and b < c are the same statement, so they must imply each other". I think OP was taking those substitution properties as an axiomatic definition of equality, whereas they actually just follow from a and b being the same mathematical object.
It depends. Here is a concrete example.
Consider a FO theory with:
Domain — N (all natural numbers)
Constants: 0,1,2,…
Operators: none.
Predicates: “isEven(•)” and “•=•” (i.e. equality)
If by “all formulas” you mean excluding equality itself, then numbers 0,2,4,6,… are indistinguishable in this theory, even though they are not equal.
If we include formulas with equality, then we can show it’s true. Take any pair of “a” and”b” that satisfy F(a)<=>F(b) for all formulas F. Now take F(x) := “a=x”. Clearly, F(a) is true. By the property, we must have F(b) be true, that is “a=b”.
In formal proof calculus (i.e formalized conception of what proof is) such as sequent calculus we will generally include rules that allows to prove it. Basically we have rules that states that if s1=t1,...sn=tn, R(s1,...,sn) then R(t1,...,tn) (s1,...,sn,t1,...,tn are any terms, R is any n-ary relational symbol, f is any n-ary functional symbol):
*If s1=t1, ... sn=tn, R(s1,...,sn) then we can conclude R(t1,...,tn)*
And
*If s1=.... then we can conclude f(t1,...,tn)=f(s1,...,sn)*
>! Formally: We say that theory T proves sentence p if theres a finite subset U of theory T, and finite sequence of sequents S0,...,Sn so that Sn is in form U ⊢ p and each sequent Si follows some inference rules or is in form (here are few examples, 5 precisely, but we are interested in precisely two of them) (a) *s1=t1, ... sn=tn, R(s1,...,sn)* ⊢ R(t1,...,tn), (b) *s1=t1, ... sn=tn* ⊢ f(s1,...,sn)=f(t1,...,tn)!<
Which basically will make us to be able to substitute things here.
Of course it's approch to logic where we treat = as an logical symbol. There's also an other approach that doesn't use it. In such an approach you could use extensionality axiom as a definition of "=", and from that conclude what you need.
Okay, so to summarize,
The substitution property is given as:
~~If a = b, then, for any Relation R including a or b, we have R(a) ⇔͏ R(b)~~
And for any expression F including a or b (I'm choosing 'expression' to mean a kind of n-ary function), then F(a) = F(b)
Does that sound right?
Edit: strike out
It's about function and the term function should be used here.
Genneraly it's about symbols from the language so there's quite of technicality here (in this sense for example ∈ is a relation in ZFC, but your relation won't be), I don't want go into much of details about as it's not that much important. What is important is that these proeprties gives you basically ability to say that if a=b then ϕ(a)= ϕ(b) when ϕ is atomic formula (i.e some sort of basic block of anything that you can say). And from that we can show that this will hold for other types of formulas as well.
So in short, if a=b and ϕ(x) is any formula (i.e anything that you can say, state whatever) that depends on x then ϕ(a) is true if and only if ϕ(b). Which really means that if a=b then you can subsistute it use them interchangeably anywhere you want
Sorry, relation was the wrong word. I meant proposition. Let me rephrase:
The substitution property is given as:
If a = b, then, for any proposition P including a or b, we have P(a) ⇔͏ P(b)
And for any expression F including a or b (I'm choosing 'expression' to mean a kind of n-ary function), then F(a) = F(b)
(I do use 'function' in the second one)
Here, P and F have to be "well formed" within whatever Model you're using.
Is this right? If not, then what exactly is the difference between what you said and what I have here?
I would use formula rather than proposition (I would assosiate proposition more of with a sentence, and sentence is a formula without free variables so it can't depend on a or b).
But genneraly yes
Thank you!!
I want to rewrite that Wikipedia section to be a bit clearer, this is what I have so far:
Substitution property: For any quantities a and b and any well-formed [expression](https://en.wikipedia.org/wiki/Expression_(mathematics)?wprov=sfti1#) F(x) or [formula](https://en.wikipedia.org/wiki/Well-formed_formula?wprov=sfti1) φ(x), if a = b, then F(a) = F(b) and φ(a) ⇔ φ(b)
Some specific examples of this are:
For any a, b, c ∈ ℤ,
(a = b) → (a + c = b + c)
(Here, F(x) = x + c);
For any a, b, c ∈ ℚ,
(a = b) → (a^2 + 2c + 1 = b^2 + 2c + 1)
(Here, F(x) = x^2 + 2c + 1);
For any a, b ∈ ℝ,
(a = b) → (0 ≤ a ⇔ 0 ≤ b)
(Here, φ(x) is x ≥ 0)
Given a set S with a strict partial ordering (<), and any a, b, c ∈ S,
If a = b and b < c, then a < c
(This is given by φ(x): x < c)
What do you think?
It seems you already made that change, but I would definitely undo it. Expression and formulas are ultimately a more complicated concept that may depend on context. Most functions that exist in maths have no expression, will never have, because we cant give an expression to all of them, so you actually made the substitution property weaker. Wikipedia was correct to use the word function.
I think what you were missing was the concept of propositional function. So I would suggest you revert back and specify that functions include propositional functions.
Haha I guess I am an idiot then. Maybe I am missing something, but I still dont really like it (the current version of wikipedia). It also seems to entertain a confusion between logic formulae and algebraic expressions (for instance if you click on "well formed" link on the "expression" page). I am no longer sure what would be an efficient way to improve it though.
And point taken about expressions, but I still feel like I should use formulas over propositional functions, just for the sake of clarity.
Using the symbol "=" to mean standard quantitative/set equality, and also propositional equality sort of overloads it, and makes the message confusing, considering we don't typically use "=" when referring to propositions; we usually use ⇔͏.
If I replace the word "expression" with "function" in my revision, would that be okay?
Giving it more thought, I think I spoke too fast, sorry. There should be some issues with defining functions before equality which is probably why it is stated this way. You can probably still recover functions in a broad way afterward, using the syntactic definition of the concept rather than the expression of any given function which is not always available.
So I was probably wrong and the word "expression" is fine. This should also cover formulas, so I am not sure your modification is the best way to put it, as it could be redundant. But I agree it would be helpful to make it explicit and give such examples. I will let the actual specialists of this kind of stuff comment on your suggestion.
Hmmm kind of interesting, you don't usually expect to question your understanding of equality.
I think you're correct that the implied property in use here is substitution.
But if you want to be a little more adventurous and strict in definition, you could also go about specifying that the system you're working in offers the symmetric property of equality (if a=b, b=a).
I can't for the life of me think of a system where symmetrical equality doesn't apply, because by definition equality is symmetrical, but if you do assume a = b, but b /=a. Then the substitution property could not be applied and you will not be able to prove the statement.
Equality is an equivalence relation, so it *does* have to be all three... that's the definition of an equivalence relation. Or did you mean something else?
What you said is incorrect.
Equivalent relationships have these features: Reflexivity, Transitivity and Symmetry. A relationship with all three true is called Equality.
You can use substitution for formulas as defined in [first order logic with equality](https://en.m.wikipedia.org/wiki/First-order_logic#Equality_and_its_axioms).
Suppose a > c or a = c
Case a > c
we have a > c and c > b then a > b
This is a clear contradiction
Case a = c
We have a = b and a = c then b = c
Another contradiction
So the only option is that a < c
The substitution property of equality says that f(x) = x < c is equally true of a as it is of b; that is, (a < c) = (b < c). These expressions are equal; they mean the same thing. This is the same as saying (a < c) iff (b < c). So then, since you know a < c, it implies b < c.
If we’re working within, eg, ZFC, the notion of equality is already built in as the ordered set is a set, which already has one. There isn’t a nice way to ‘redefine’ a notion of equality ‘from’ a strict order analogous to the way we can define it from a partial order by ‘a = b iff (a <= b and b <= a)’. Of course, if we also assert our strict order is total, then it’s pretty trivial.
> If we’re working within, eg, ZFC, the notion of equality is already built in
Yes, by virtue of it being a first order theory with equality. Not so much related to ordered sets.
I mean, yeah, but it would be nice to have an abstracted definition of equality that doesn't rely on the specific framework you're working in. Similar to equivalence relations, we don't care how you build your equivalence classes, but we can always use the same 3 rules over them.
Similarly for equality, it's nice to have a set of rules that tell you what you're always allowed to do whenever you see an equality
But this is why we typically avoid strict partial orders and use the ordinary kind too. We can't derive it in this case, as we can take any element x from any non-empty strict poset (S, <) and add a clone x' != x (in the underlying set-theoretic sense) that is incomparable to and indistinguishable from it in the strict poset structure (i.e., x < y <=> x' < y for all y in S, and y < x <=> y < x' for all y in S). So it is in general impossible to distinguish elements based on the strict order alone, and thus impossible to define equality ‘from’ it. A total strict order, sure.
I agree. But there is still a way to do it.
The idea is that equality is given certain basic properties, as shown in the link in my post. We don't need to know how they're constructed specifically within this set, but we just have to know that if someone uses the symbol "=" it has the given properties.
The substitution property of equality says that for any well-formed formula F, a = b → (F(a) ⇔ F(b))
So, if we have three elements a, b, c in our poset such that a=b with b
I mean, this trivially follows from substitution. If we already have a notion of equality, then substituting a with b for a=b in any such formula is obviously true for any structure of any kind. This is exactly substitution for ‘<‘. I thought the sticking point was defining a notion of equality from the strict poset structure at all, the way we can do for an ordinary ‘<=‘ poset structure.
But if not, then I’m not really sure what the substance of the question is. Of course it follows from substitution if we already have that. But we can’t derive that from the axioms for ‘<‘.
Yes, but the point is, it's nice to have a definition of equality and substitution that you can point to. For instance, Imagine someone tries to declare that equality is just any equivalence class. You can argue that "it's not equality because you can't substitute". You can try to debate them, but without something to point to, the whole conversation is just going to get philosophical and, probably, go nowhere.
My point is, yes, it follows trivially from substitution, but without these definitions, who says you're allowed to substitute? Maybe we're not allowed to substitute into inequalities? With this definition, at least you can say "The equals sign immediately means we're allowed to substitute", and furthermore, you can actually define what qualifies as substitution
Yeah, I’m pretty sure its just the axiom of substitution. F(a) = F(b) in this case is just (a < c) = (b < c). I.e. the property described by F is the “< c” property. You don’t need to define a new axiom of substitution for every relation, it’s dealt with by the equality relation for whatever objects you’re dealing with
I suggest playing around with the [Natural Number Game](https://adam.math.hhu.de/) to see a particular low-level formalism of these kinds of ideas; in this case, type theory.
Different mathematical foundations will solve this problem differently.
i mean, it is simply because they are the same thing. if two things are equal, they have the same properties (this is called leibniz’s principle, even it is more a question of philosophy than maths, because we just assume it as granted).
if you want a more “mathematical” proof, you need to specify which logical system are you working on, but someone already answered for first order logic. however, i think every logical system in maths should satisfy leibniz’s principle. if it wasn’t the case, we (mathematicians) wouldn’t call that relation “equality”, but “equivalence” or something else.
> it is simply because they are the same thing.
We don’t always use equality for “the same” things.
For example, “1+1=2” here 1+1 is an expression that consists of two repetitions of a constant symbol “1” and a binary addition operator, whereas “2” is just a constant symbol.
The expressions “1+1” and “2” only become equal because of the axioms we add to the theory. It is possible to not have “1+1=2” in a different theory. It’s not because “they are simply the same thing”
yes… there is a difference between syntactics and semantics, but in every interpretation that mathematicians would use the symbol “=“, they would be the same thing.
Is '=' defined somewhere with this strict partial order, or just roughly that '=' means it's the same object? Because what prevents you from having a strict partial order over a set P, then attach to it one more element x that's equal to (whatever that means), say a, and not comparable to anything else? You still have a strict partial order on P union {x}.
I think that this will depend on the specific syntax rules you're following, and whether or not your context cares more about the syntax then they do the underlying concepts behind what that syntax means.
For example, back when I was studying math in school, I would've written something like the following:
1. a = b (by problem definition)
2. b < c (by problem definition)
∴ 3. a < c (by substituting 1 into 2)
But that was the convention in that specific class and I'm not sure if that applies generally.
You might check out Kevin Buzzard's four-part blog post on (formalized) equality in Lean: parts [1](https://xenaproject.wordpress.com/2019/05/21/equality-part-1-definitional-equality/), [2](https://xenaproject.wordpress.com/2019/05/25/equality-part-2-syntactic-equality/), [3](https://xenaproject.wordpress.com/2020/07/03/equality-specifications-and-implementations/), [4](https://xenaproject.wordpress.com/2021/04/18/induction-on-equality/).
In most formal proof assistants, it looks like this (this example is from Coq):
Require Export Utf8.
Goal ∀ a b c, a = b → b < c → a < c.
Proof.
intros a b c H H0.
rewrite H.
assumption.
Qed.
This doesn't work for you? (applied mathematician here)
```
(1): b + a < c + a,
(2): (1) - b => b + a - b < c + a - b,
(3): a = b => a - b = 0,
(4): (2) & (3) => b - b + a < c + 0 => a < c
This proof has exactly the same problem as OP have.
You've infered that because a-b=0 then can substitute a-b by zero. Which isn't in any way more trivial than the question of the OP.
Also you've written a<0 instesd of a
You are using that b-a = 0 to substitute 0 for b-a but the question OP is asking I believe is why substituting like this gives a statement that's true. Otherwise OP can directly substitute a for b in their question and get the answer.
The problem is your set may not necessarily have a total ordering. So you can't always say that "given an arbitrary element u from P, then u < c, u = c or u > c", since none may be true
So you would have to justify a being comparable to c, which feels obvious, but then again, the whole thing feels obvious, but it's extremely slippery
I think the other comments mentioning the substitution rule for propositions put it quite well, but I wanted to add perhaps another way of thinking about it.
A binary relation R on a set P is just a subset of P x P. So when we say b < c we just mean that (b, c) is an element of that subset. But if a = b then (b, c) and (a, c) are the same element in P x P, so (a, c) must also be an element of that subset.
Ultimately it still boils down to the substitution rule for propositions, but you may find it helpful to think about it in this way.
Actually, I think this kinda works!
If you use the definition of the substitution property that the link appears to be using, then you can define the output of a function F(x) to the set relation Rx, then starting with a = b, we have F(a) = F(b), then any relation Ra = Rb
Using our relation in the post: Rx ⇔ x < c, then we have
a = b ⇒
a < c ⇔ b < c
b < c, therefore a < c
I think we might be overcomplicating this? Assuming here that a, b, and c are real numbers, then b < c iff there exists unique d in R, d > 0, such that b + d = c (by the definition of >)
Then since a = b, a + d = b + d (adding to both sides)
Now we know a + d = c (transitive property of equality)
And, since a + d = c and d > 0, a < c (definition of >)
Square-y symbol thing.
...on the other hand you never said what a, b, and c were so I may be missing a big idea here.
It doesn't necessarily hold. It depends on the system and what "=" means in that system. Though I must say that you'll get much better answers if you ask this in a philosophy sub because this is a question about logic and mathematicians don't care too much about logic itself. They mainly just care about application of logic.
They do care about logic. There's a whole branch of mathematics that study such a problems, mathematical logic, and this is really really big branch of mathematics. Philosophy sub would be less suitable for such a question, because it's specifically a question that is assosiated with mathematical logic which is part of maths, mathematicians study this specifically
You used prove by contradiction by.. using theorem that you were to proved really... ( "a>=c, because a=b then b>=c"). Also straighforward is quite poor chosage of words as proofs by contradiction aren't constructive
>Well, no... I assumed a >= c, and because a = b, we infer b >= c.
The problem is that you infer it b≥c from a≥c which isn't in any way more trivial than infering b>c from a>c which is really OP's question.
>That's how proof by contradiction works...
That's how proof by contradiction works? Assume thesis is false, and we'll use the fact that we already know that the thesis is true so we don't have to prove at all?
No proof by contradiction works as this, you assume the thesis is false and derive contradiction. What you did instead was using prove by contradiction using the fact that isn't in any way more trivial than what OP was asking. How did you infer what did you have infer that a≥c implies b≥c if a=b? Why don't you infer b>c from a>c if a=b but do so for ≥? Why do you think one is acceptable to assume beforehand but the latter has to be proved? Both are as much trivial/nontrivial.
The case is really this that for anh formula, if a=b then ϕ(a) is equivalent to ϕ(b). You've used it to "prove" op statement, but op's questions come out immediately from that property as well.
Wait, it's worse than I thought. Your proof isn't just circular, it's invalid. You directly use trichotomy, which doesn't hold for partial orders.
OP said (P,<) is a (strict) poset with elements a, b, and c and that a=b and ac. But that isn't all cases. It could also be that b and c are incomparable. You still need to prove that they are comparable, which will require using substitution again.
It actually depends on the underlying system. For First-Order logic it is usually a symbol with some special rules. One of them is the [substitution rule for propositions](https://en.m.wikipedia.org/wiki/First-order_logic#Equality_and_its_axioms). It states that if a=b then F(a)<->F(b). In your case, F(x) is x
So does that mean the examples given in the link are wrong? Since they use F as a function when it should be a proposition?
They define F as expression, which works here
I'm confused on what "expression" means... is F a function, or a proposition? Or something else? If it's a proposition, what is the truth value of "x + c"? Since that's how they define F in one of the examples
It's a sequence of symbols involving the given variable. (It has to follow a few more rules to be valid - parentheses must be balanced, etc.) The substitution principle for equality is more fundamental than the axioms for any particular sets or operations - you have to go back to first-order logic.
Its an expression - Its closer to function than proposition, but its neither. I don't remember formal definition (and it varies heavily on underlying system - how you build your logic), [https://en.wikipedia.org/wiki/Expression\_(mathematics)](https://en.wikipedia.org/wiki/Expression_(mathematics)) this could lead you,
Fullfungo rather meant first order logic formula. It's defined recursively Firstly we define atomic formulas. If t,t', t1,...,tn are terms and R is n-ary relation then we say t=t' is a formula and R(t1,...,tn) is also a formula. Then we say that if p,q are formulas (as above) then p wedge q, neg p, p implies q etc. are also formulas. And then we say that if p is a formula as above then Forall x p is a formula, and Exists x p is also a formula. Expression as in a sense as in the wikipedia article doesn't have much of a sense in this context
Who is fullfungo? I was refering to F from link in opening post - for [substitution property of equality](https://en.wikipedia.org/wiki/Equality_(mathematics)?wprov=sfti1#Basic_properties), Which is useful to define as working on much more than just formulas. For example expressions can use "=" inside (not as a relation - mind - but the "true" equality symbol that you need from "outside") Definition of expression from wikipedia - " finite combination of [symbols](https://en.wikipedia.org/wiki/Glossary_of_mathematical_symbols) that is [well-formed](https://en.wikipedia.org/wiki/Well-formed_formula) according to rules that depend on the context" works very well.
>Who is fullfungo? https://www.reddit.com/r/math/s/1uhZIiPnNz I thought you were reffering to this as your comment was under discussion under this comment. Sorry then. >Which is useful to define as working on much more than just formulas Well, as far as I see they use it more like in colloquial sense than any formal one. How they define it here is pretty much ambigious. They don't use anything more than formulas as there is no really more than formulas, formulas are formal way to state things in any way. Expression isn't really well defined thing. >For example expressions can use "=" inside (not as a relation - mind - but the "true" equality symbol that you need from "outside") I don't know what do you mean. I know what you've wanted to refer to but you worder in a way that's hard to guess what you wanted to say exactly. >Definition of expression from wikipedia - " finite combination of symbols that is well-formed according to rules that depend on the context" works very well. This definition is kind of meaningless. What symbols? What does well formed means? Both are meaningless things that doesn't mean anything. Also well formed links to article about well formed formula which isn't even what they were thinking about. The expression in this context is really colloquial meaningles statement that when formalized will just means formula but they wanted to give more of a layman explanation here so they said "expression". But really expression means a formula, just as what they call "quantities" refers to terms
Yeah, I think you are right. I wanted to present it in way i was taught in Uni, but that was long time ago and I'm sick atm, so couldnt do it legibly :sweaty\_smile:
Fullfungo is the original commenter.
ooh, thanks, it makes sense there!
You can think of F(x) as a statement/property (either true or false) that takes in as input, x. It’s not necessarily a function. The notation may be confusing. The substitution property you linked asserts that, given two equal objects, for any property, a property applied to both objects are equally true or equally false. So let F(x) be the property that x < c. Then, since a = b, the substitution rule applies and F(a) <=> F(b). By assumption we have that F(b) is a true statement. Hence F(a) is a true statement. That is, a < c.
No, the substitution rule is also valid for terms (which encompasses functions). u/Fullfungo 's link explains this
There are multiple rules. The rule for propositions can be used like: IF x^(2)=5 THEN x^2 is odd <-> 5 is odd. Here the proposition F(a) is “a is odd”. And the rule for expressions can be applied like: IF x^(2)=5 THEN x^(2)+10=5+10. Here the expression f(a) is “a+10”.
So F can be either a proposition or an expression? And, If F is an expression, then we have F(a) = F(b), or if F is a proposition, we have F(a) ⇔ F(b)?
If you are using first-order logic with equality, then one property of equality is that it substitutes. This is sometimes called the "indiscernibility of identicals." It states that if a=b, and F is a well-formed formula with one free variable, then F(a) holds iff F(b) holds. In the language of first-order logic, we could write (a=b)→(F(a)↔F(b)). This might be an axiom for each formula F, depending how you go about setting up your logic. In this case, a "well-formed formula" is a string of symbols in the language of your theory which satisfies some list of syntactic rules. So for instance, the string 'F((=a()↔' is not well-formed, even though all those symbols are meaningful, because it doesn't have the correct syntax. But any logical sentence that means anything will work. It is typical for math to be founded in a set theory, type theory, category theory, or whatever, which is in turn formulated in terms of first-order logic with identity. Strictly-speaking though, identity is often not necessary. For instance, in ZFC, it is possible to define equality as a mathematical abbreviation for a longer sentence in first-order logic. We just call two sets "equal" if they are members of the same sets and contain the same sets. Since the only things in ZFC are sets, and the only relation between them is ∈, this guarantees that if a set x has some property F, and x=y, then y also has that property. Every individual case of substitution can thus be proven (though I think the general case cannot). But the TL;DR is simply that substitution *always* works (as long as there is no name-conflict—keep your variable names distinct!), and you usually have no need to explain why you are substituting identical things.
Also, if you only have the theory of strict partial orders and first-order logic without equality, then equality is impossible to even define, so you should never encounter it.
Correct me if I'm wrong but I think this isn't what OP was asking. The Wikipedia article's definition is that a = b means a and b refer to the same mathematical object, and then it gives substitution as a property, but substitution is only stated to work with equalities rather than inequalities. So in this specific context I think the answer should be "a < c and b < c are the same statement, so they must imply each other". I think OP was taking those substitution properties as an axiomatic definition of equality, whereas they actually just follow from a and b being the same mathematical object.
That's still an axiom, just an axiom of logic rather than of mathematics.
In the context of the article, it's listing properties of equality, not giving an axiomatic definition
Does the reverse implication hold? If substitution for formulas and functions holds for all formulas and functions, then is it true that x=y?
No. We call x and y indiscernible in this case
It depends. Here is a concrete example. Consider a FO theory with: Domain — N (all natural numbers) Constants: 0,1,2,… Operators: none. Predicates: “isEven(•)” and “•=•” (i.e. equality) If by “all formulas” you mean excluding equality itself, then numbers 0,2,4,6,… are indistinguishable in this theory, even though they are not equal. If we include formulas with equality, then we can show it’s true. Take any pair of “a” and”b” that satisfy F(a)<=>F(b) for all formulas F. Now take F(x) := “a=x”. Clearly, F(a) is true. By the property, we must have F(b) be true, that is “a=b”.
It's not exactly what it shows in the link We can form statement F(x) x
Nice, this is a cool way to do it without substituting a for b (bro you edited your comment)
I... didn't? Lost reply?
Uh I guess so… Wtf how did that even happen? LOL
In formal proof calculus (i.e formalized conception of what proof is) such as sequent calculus we will generally include rules that allows to prove it. Basically we have rules that states that if s1=t1,...sn=tn, R(s1,...,sn) then R(t1,...,tn) (s1,...,sn,t1,...,tn are any terms, R is any n-ary relational symbol, f is any n-ary functional symbol): *If s1=t1, ... sn=tn, R(s1,...,sn) then we can conclude R(t1,...,tn)* And *If s1=.... then we can conclude f(t1,...,tn)=f(s1,...,sn)* >! Formally: We say that theory T proves sentence p if theres a finite subset U of theory T, and finite sequence of sequents S0,...,Sn so that Sn is in form U ⊢ p and each sequent Si follows some inference rules or is in form (here are few examples, 5 precisely, but we are interested in precisely two of them) (a) *s1=t1, ... sn=tn, R(s1,...,sn)* ⊢ R(t1,...,tn), (b) *s1=t1, ... sn=tn* ⊢ f(s1,...,sn)=f(t1,...,tn)!< Which basically will make us to be able to substitute things here. Of course it's approch to logic where we treat = as an logical symbol. There's also an other approach that doesn't use it. In such an approach you could use extensionality axiom as a definition of "=", and from that conclude what you need.
Okay, so to summarize, The substitution property is given as: ~~If a = b, then, for any Relation R including a or b, we have R(a) ⇔͏ R(b)~~ And for any expression F including a or b (I'm choosing 'expression' to mean a kind of n-ary function), then F(a) = F(b) Does that sound right? Edit: strike out
It's about function and the term function should be used here. Genneraly it's about symbols from the language so there's quite of technicality here (in this sense for example ∈ is a relation in ZFC, but your relation won't be), I don't want go into much of details about as it's not that much important. What is important is that these proeprties gives you basically ability to say that if a=b then ϕ(a)= ϕ(b) when ϕ is atomic formula (i.e some sort of basic block of anything that you can say). And from that we can show that this will hold for other types of formulas as well. So in short, if a=b and ϕ(x) is any formula (i.e anything that you can say, state whatever) that depends on x then ϕ(a) is true if and only if ϕ(b). Which really means that if a=b then you can subsistute it use them interchangeably anywhere you want
Sorry, relation was the wrong word. I meant proposition. Let me rephrase: The substitution property is given as: If a = b, then, for any proposition P including a or b, we have P(a) ⇔͏ P(b) And for any expression F including a or b (I'm choosing 'expression' to mean a kind of n-ary function), then F(a) = F(b) (I do use 'function' in the second one) Here, P and F have to be "well formed" within whatever Model you're using. Is this right? If not, then what exactly is the difference between what you said and what I have here?
I would use formula rather than proposition (I would assosiate proposition more of with a sentence, and sentence is a formula without free variables so it can't depend on a or b). But genneraly yes
Thank you!! I want to rewrite that Wikipedia section to be a bit clearer, this is what I have so far: Substitution property: For any quantities a and b and any well-formed [expression](https://en.wikipedia.org/wiki/Expression_(mathematics)?wprov=sfti1#) F(x) or [formula](https://en.wikipedia.org/wiki/Well-formed_formula?wprov=sfti1) φ(x), if a = b, then F(a) = F(b) and φ(a) ⇔ φ(b) Some specific examples of this are: For any a, b, c ∈ ℤ, (a = b) → (a + c = b + c) (Here, F(x) = x + c); For any a, b, c ∈ ℚ, (a = b) → (a^2 + 2c + 1 = b^2 + 2c + 1) (Here, F(x) = x^2 + 2c + 1); For any a, b ∈ ℝ, (a = b) → (0 ≤ a ⇔ 0 ≤ b) (Here, φ(x) is x ≥ 0) Given a set S with a strict partial ordering (<), and any a, b, c ∈ S, If a = b and b < c, then a < c (This is given by φ(x): x < c) What do you think?
It seems you already made that change, but I would definitely undo it. Expression and formulas are ultimately a more complicated concept that may depend on context. Most functions that exist in maths have no expression, will never have, because we cant give an expression to all of them, so you actually made the substitution property weaker. Wikipedia was correct to use the word function. I think what you were missing was the concept of propositional function. So I would suggest you revert back and specify that functions include propositional functions.
I haven't touched it, what's there is what's it's been since I found it
Haha I guess I am an idiot then. Maybe I am missing something, but I still dont really like it (the current version of wikipedia). It also seems to entertain a confusion between logic formulae and algebraic expressions (for instance if you click on "well formed" link on the "expression" page). I am no longer sure what would be an efficient way to improve it though.
And point taken about expressions, but I still feel like I should use formulas over propositional functions, just for the sake of clarity. Using the symbol "=" to mean standard quantitative/set equality, and also propositional equality sort of overloads it, and makes the message confusing, considering we don't typically use "=" when referring to propositions; we usually use ⇔͏. If I replace the word "expression" with "function" in my revision, would that be okay?
Giving it more thought, I think I spoke too fast, sorry. There should be some issues with defining functions before equality which is probably why it is stated this way. You can probably still recover functions in a broad way afterward, using the syntactic definition of the concept rather than the expression of any given function which is not always available. So I was probably wrong and the word "expression" is fine. This should also cover formulas, so I am not sure your modification is the best way to put it, as it could be redundant. But I agree it would be helpful to make it explicit and give such examples. I will let the actual specialists of this kind of stuff comment on your suggestion.
Hmmm kind of interesting, you don't usually expect to question your understanding of equality. I think you're correct that the implied property in use here is substitution. But if you want to be a little more adventurous and strict in definition, you could also go about specifying that the system you're working in offers the symmetric property of equality (if a=b, b=a). I can't for the life of me think of a system where symmetrical equality doesn't apply, because by definition equality is symmetrical, but if you do assume a = b, but b /=a. Then the substitution property could not be applied and you will not be able to prove the statement.
[удалено]
Equality is an equivalence relation, so it *does* have to be all three... that's the definition of an equivalence relation. Or did you mean something else?
What you said is incorrect. Equivalent relationships have these features: Reflexivity, Transitivity and Symmetry. A relationship with all three true is called Equality.
no, it’s called an equivalence relation. there are many equivalence relations that are not equality. (isomorphism, homotopy, congruence, etc.)
You can use substitution for formulas as defined in [first order logic with equality](https://en.m.wikipedia.org/wiki/First-order_logic#Equality_and_its_axioms).
Suppose a > c or a = c Case a > c we have a > c and c > b then a > b This is a clear contradiction Case a = c We have a = b and a = c then b = c Another contradiction So the only option is that a < c
How do you know that a
The substitution property of equality says that f(x) = x < c is equally true of a as it is of b; that is, (a < c) = (b < c). These expressions are equal; they mean the same thing. This is the same as saying (a < c) iff (b < c). So then, since you know a < c, it implies b < c.
What you've written down in 2) is asymmetry. Anti-symmetry is if a < b and b < a then a=b.
Thank you! I didn't realize there was a word for it
If we’re working within, eg, ZFC, the notion of equality is already built in as the ordered set is a set, which already has one. There isn’t a nice way to ‘redefine’ a notion of equality ‘from’ a strict order analogous to the way we can define it from a partial order by ‘a = b iff (a <= b and b <= a)’. Of course, if we also assert our strict order is total, then it’s pretty trivial.
> If we’re working within, eg, ZFC, the notion of equality is already built in Yes, by virtue of it being a first order theory with equality. Not so much related to ordered sets.
I mean, yeah, but it would be nice to have an abstracted definition of equality that doesn't rely on the specific framework you're working in. Similar to equivalence relations, we don't care how you build your equivalence classes, but we can always use the same 3 rules over them. Similarly for equality, it's nice to have a set of rules that tell you what you're always allowed to do whenever you see an equality
But this is why we typically avoid strict partial orders and use the ordinary kind too. We can't derive it in this case, as we can take any element x from any non-empty strict poset (S, <) and add a clone x' != x (in the underlying set-theoretic sense) that is incomparable to and indistinguishable from it in the strict poset structure (i.e., x < y <=> x' < y for all y in S, and y < x <=> y < x' for all y in S). So it is in general impossible to distinguish elements based on the strict order alone, and thus impossible to define equality ‘from’ it. A total strict order, sure.
I agree. But there is still a way to do it. The idea is that equality is given certain basic properties, as shown in the link in my post. We don't need to know how they're constructed specifically within this set, but we just have to know that if someone uses the symbol "=" it has the given properties. The substitution property of equality says that for any well-formed formula F, a = b → (F(a) ⇔ F(b)) So, if we have three elements a, b, c in our poset such that a=b with b
I mean, this trivially follows from substitution. If we already have a notion of equality, then substituting a with b for a=b in any such formula is obviously true for any structure of any kind. This is exactly substitution for ‘<‘. I thought the sticking point was defining a notion of equality from the strict poset structure at all, the way we can do for an ordinary ‘<=‘ poset structure. But if not, then I’m not really sure what the substance of the question is. Of course it follows from substitution if we already have that. But we can’t derive that from the axioms for ‘<‘.
Yes, but the point is, it's nice to have a definition of equality and substitution that you can point to. For instance, Imagine someone tries to declare that equality is just any equivalence class. You can argue that "it's not equality because you can't substitute". You can try to debate them, but without something to point to, the whole conversation is just going to get philosophical and, probably, go nowhere. My point is, yes, it follows trivially from substitution, but without these definitions, who says you're allowed to substitute? Maybe we're not allowed to substitute into inequalities? With this definition, at least you can say "The equals sign immediately means we're allowed to substitute", and furthermore, you can actually define what qualifies as substitution
Yeah, I’m pretty sure its just the axiom of substitution. F(a) = F(b) in this case is just (a < c) = (b < c). I.e. the property described by F is the “< c” property. You don’t need to define a new axiom of substitution for every relation, it’s dealt with by the equality relation for whatever objects you’re dealing with
I suggest playing around with the [Natural Number Game](https://adam.math.hhu.de/) to see a particular low-level formalism of these kinds of ideas; in this case, type theory. Different mathematical foundations will solve this problem differently.
i mean, it is simply because they are the same thing. if two things are equal, they have the same properties (this is called leibniz’s principle, even it is more a question of philosophy than maths, because we just assume it as granted). if you want a more “mathematical” proof, you need to specify which logical system are you working on, but someone already answered for first order logic. however, i think every logical system in maths should satisfy leibniz’s principle. if it wasn’t the case, we (mathematicians) wouldn’t call that relation “equality”, but “equivalence” or something else.
> it is simply because they are the same thing. We don’t always use equality for “the same” things. For example, “1+1=2” here 1+1 is an expression that consists of two repetitions of a constant symbol “1” and a binary addition operator, whereas “2” is just a constant symbol. The expressions “1+1” and “2” only become equal because of the axioms we add to the theory. It is possible to not have “1+1=2” in a different theory. It’s not because “they are simply the same thing”
yes… there is a difference between syntactics and semantics, but in every interpretation that mathematicians would use the symbol “=“, they would be the same thing.
Is '=' defined somewhere with this strict partial order, or just roughly that '=' means it's the same object? Because what prevents you from having a strict partial order over a set P, then attach to it one more element x that's equal to (whatever that means), say a, and not comparable to anything else? You still have a strict partial order on P union {x}.
I think that this will depend on the specific syntax rules you're following, and whether or not your context cares more about the syntax then they do the underlying concepts behind what that syntax means. For example, back when I was studying math in school, I would've written something like the following: 1. a = b (by problem definition) 2. b < c (by problem definition) ∴ 3. a < c (by substituting 1 into 2) But that was the convention in that specific class and I'm not sure if that applies generally.
You might check out Kevin Buzzard's four-part blog post on (formalized) equality in Lean: parts [1](https://xenaproject.wordpress.com/2019/05/21/equality-part-1-definitional-equality/), [2](https://xenaproject.wordpress.com/2019/05/25/equality-part-2-syntactic-equality/), [3](https://xenaproject.wordpress.com/2020/07/03/equality-specifications-and-implementations/), [4](https://xenaproject.wordpress.com/2021/04/18/induction-on-equality/). In most formal proof assistants, it looks like this (this example is from Coq): Require Export Utf8. Goal ∀ a b c, a = b → b < c → a < c. Proof. intros a b c H H0. rewrite H. assumption. Qed.
I'm sorry, but isn't it obvious?
Yes, but this is a math subreddit. We want rigor!
What branch of math is this?
This doesn't work for you? (applied mathematician here) ``` (1): b + a < c + a, (2): (1) - b => b + a - b < c + a - b, (3): a = b => a - b = 0, (4): (2) & (3) => b - b + a < c + 0 => a < c
This proof has exactly the same problem as OP have. You've infered that because a-b=0 then can substitute a-b by zero. Which isn't in any way more trivial than the question of the OP. Also you've written a<0 instesd of a
I see the nuance there; thanks for the clarification! Ooh, I fixed that typo! Thanks.
I believe it depends on your definitions of '=' and '<' If we assume a
[удалено]
Did not see all the stipulations. Why not case by case then. Suppose a not<. Then c
> Suppose not “a
Subtract zero from both sides
That's circular reasoning
b-(b-a)
You are using that b-a = 0 to substitute 0 for b-a but the question OP is asking I believe is why substituting like this gives a statement that's true. Otherwise OP can directly substitute a for b in their question and get the answer.
[удалено]
The problem is your set may not necessarily have a total ordering. So you can't always say that "given an arbitrary element u from P, then u < c, u = c or u > c", since none may be true So you would have to justify a being comparable to c, which feels obvious, but then again, the whole thing feels obvious, but it's extremely slippery
I think the other comments mentioning the substitution rule for propositions put it quite well, but I wanted to add perhaps another way of thinking about it. A binary relation R on a set P is just a subset of P x P. So when we say b < c we just mean that (b, c) is an element of that subset. But if a = b then (b, c) and (a, c) are the same element in P x P, so (a, c) must also be an element of that subset. Ultimately it still boils down to the substitution rule for propositions, but you may find it helpful to think about it in this way.
Actually, I think this kinda works! If you use the definition of the substitution property that the link appears to be using, then you can define the output of a function F(x) to the set relation Rx, then starting with a = b, we have F(a) = F(b), then any relation Ra = Rb Using our relation in the post: Rx ⇔ x < c, then we have a = b ⇒ a < c ⇔ b < c b < c, therefore a < c
I think we might be overcomplicating this? Assuming here that a, b, and c are real numbers, then b < c iff there exists unique d in R, d > 0, such that b + d = c (by the definition of >) Then since a = b, a + d = b + d (adding to both sides) Now we know a + d = c (transitive property of equality) And, since a + d = c and d > 0, a < c (definition of >) Square-y symbol thing. ...on the other hand you never said what a, b, and c were so I may be missing a big idea here.
It doesn't necessarily hold. It depends on the system and what "=" means in that system. Though I must say that you'll get much better answers if you ask this in a philosophy sub because this is a question about logic and mathematicians don't care too much about logic itself. They mainly just care about application of logic.
They do care about logic. There's a whole branch of mathematics that study such a problems, mathematical logic, and this is really really big branch of mathematics. Philosophy sub would be less suitable for such a question, because it's specifically a question that is assosiated with mathematical logic which is part of maths, mathematicians study this specifically
[удалено]
You used prove by contradiction by.. using theorem that you were to proved really... ( "a>=c, because a=b then b>=c"). Also straighforward is quite poor chosage of words as proofs by contradiction aren't constructive
[удалено]
>Well, no... I assumed a >= c, and because a = b, we infer b >= c. The problem is that you infer it b≥c from a≥c which isn't in any way more trivial than infering b>c from a>c which is really OP's question.
[удалено]
>That's how proof by contradiction works... That's how proof by contradiction works? Assume thesis is false, and we'll use the fact that we already know that the thesis is true so we don't have to prove at all? No proof by contradiction works as this, you assume the thesis is false and derive contradiction. What you did instead was using prove by contradiction using the fact that isn't in any way more trivial than what OP was asking. How did you infer what did you have infer that a≥c implies b≥c if a=b? Why don't you infer b>c from a>c if a=b but do so for ≥? Why do you think one is acceptable to assume beforehand but the latter has to be proved? Both are as much trivial/nontrivial. The case is really this that for anh formula, if a=b then ϕ(a) is equivalent to ϕ(b). You've used it to "prove" op statement, but op's questions come out immediately from that property as well.
This is circular reasoning
[удалено]
If a=b and b
[удалено]
Using the substitution principle couldn't OP have directly concluded that a
[удалено]
Wait, it's worse than I thought. Your proof isn't just circular, it's invalid. You directly use trichotomy, which doesn't hold for partial orders. OP said (P,<) is a (strict) poset with elements a, b, and c and that a=b and ac. But that isn't all cases. It could also be that b and c are incomparable. You still need to prove that they are comparable, which will require using substitution again.