@user21820 :47027449 alright, this thing indeed irritates me strong enough I want to define some type of error value or whatever just to have that "aha" moment when you use the fact that you have an input in your domain of definition
Hello! So we have now two interesting topics to discuss. =)
Let's start with your question about irrationality. The thing is that if you have any property Q on S, you can prove "∀x∈S ( Q(x) ⇒ Q(x) )" without any ¬intro. So it cannot be always true that if Q is the negation of some property then proving that something satisfies Q must involve ¬intro. So we need a better way of capturing the intuitive idea.
(Same if we have an axiom that directly implies what we want.)
In particular, a context chain is a nested sequence of contexts. Let R(k) ≡ ( for every context chain C and proposition Q where C and Q have k occurrences of "¬" or "∧" or "⇒" in total, if Q is true within C then Q is provable within C ). We induct on R.
The induction is as follows. Take any context C and proposition Q with k boolean operations that is true within C.
If k=0 then trivially Q must match some assumption in C. So we can assume that k>0.
If Q is "A⇒B", then B is true within the context chain C+A, and hence B is provable within C+A by R(k−1), after which we can use ⇒intro to prove Q within C.
If Q is "¬A", then "⊥" is true within C+A, and hence provable within C+A by R(k−1), after which ¬intro yields "¬A within C.
If Q is "A∧B", then A,B are individually true within C, and hence provable within C by R(<k).
The above is for the propositional language that only permits "¬" and "∧" and "⇒" and "⊥" and atomic propositions.
To deal with "∨" in an expanded language, we separately show that "A∨B" and "¬(¬A∧¬B)" are inter-deducible in every context.
Hmm I missed a case; if Q is "⊥". Seems like this approach won't give me exactly what I want. I wanted to say that we can see that the only way to 'introduce' negation is to use ¬intro, as per the above proof, but that isn't going to work so easily as I thought, due to the missing case.
@MaliceVidrine Well I guess the motivating question is how to show that we need ¬intro to prove that sqrt(2) is irrational, namely "¬∃x,y∈N ( x·x = 2·y·y )".
Preferably, the answer should be general enough to apply to a vastly wider class of negative tautologies over many kinds of natural theories.
Oops... "¬∃x,y∈N ( x≠0 ∧ x·x = 2·y·y )".
But if you're tired, I don't mean to ask you to think about it. =)
I'm not sure I've written a proof before that would introduce a negation any other way than \neg-intro. One place I go to is to ask whether there's a proof of irrationality (in the appropriate language) using only coherent sequents -- i.e. sequents of the form P |- Q where P and Q are constructed from atomic formulae, \top, and \bot by existential quantification, conjunction, and disjunction. (and reasoning only with the sequent rules for those connectives)
The only place a "negation" could appear is in the final step, so it's a pretty nice notion of a "positive proof"
But I suspect this doesn't quite get at the question.
Phrasing that so as not to introduce universal quantification to our sequents is a little tricky. But in this case I'm not sure universal quantification is really a sticking point without implication.
@famesyasd It's not that you can't use it, but using it would be contrary to constructive proof, since the proof of the specific instance of well-ordering itself would require quite a lot of LEM besides induction.
It's just like you can remove ¬intro if you add LEM and EX, namely "⊢ A∨¬A" and "⊥ ⊢ A".
A∨¬A.
If A:
⊥. // use your proof for ( A ⊢ ⊥ ) to get this.
¬A.
If ¬A:
¬A.
¬A.
You wouldn't consider this as essentially different from using ¬intro, so just because we technically didn't use that rule doesn't mean much. The ¬intro was just hiding in LEM+EX.
Similarly, if you use well-ordering instead of induction, it essentially hides a lot of LEM.
@user638203 Are you familiar with first-order logic?
If you do, you can read the posts linked from my profile on axioms and definitions.
@user638203 You can check out the my post on introductory logic texts linked on the right. But there is a difference between using logic and analyzing logic, and one must learn to use logic before attempting to analyze it. Unfortunately all logic texts I've found don't explain how to use it.
@user638203: Do you already know propositional logic? If so, you can try to understand the rules and examples under "Natural Deduction" on my profile. If you have any specific questions, feel free to ask here. I always focus on making sure people can use logic before we move on to analyzing logic.
@famesyasd So do you get my point about well-ordering? In fact, you did the proof before, and you can see that you're using ¬intro at the 3rd-last line "r not in A". (I made a mistake at that time, it's the "r not in A" after "contradiction" that is redundant.)
@user638203 That's good, because it means you should be able to understand much of my posts on axioms and definitions. In short, axioms are assumptions, whereas definitions can be thought of as short-forms for properties or an object satisfying some property.
When you axiomatize groups, you are giving assumptions that hold for every group, and this doesn't imply that there are any groups at all.
When you define a group, you have to construct it (and, typically, show that it satisfies the group axioms).
It is true that when you define "group", you do so by saying "Define a group as a structure with one binary operation that satisfies the group axioms." But many definitions are not definitions of kinds of structures, so it's not the same.
For example, we define 2 := 1+1, and 3 := 2+1.
Ah I think I know what you're thinking... See this post which explains how we can define/introduce new symbols, which can be implemented in a formal system by allowing you to add certain axioms:
What you may be looking for in your formal system is variously called full abbreviation power or definitorial expansion. Basically, it comprises rules that allows you to create on the fly new symbols extending the original language. We need one type of rule for each kind of symbol:
$\def\eq{\left...
This may be why you think definitions are like new axioms.
But note that this is still not the same as axiomatizing structures, because that is done inside the foundational system, whereas definitions are done outside in some sense.
Let MS denote the foundational system. When you work inside MS, you can define first-order logic itself via say natural deduction, which is a system of inference rules that govern what strings are valid proofs and what strings are theorems, given any set of strings called axioms. For example MS itself can construct the set of all valid proofs and theorems for the theory of groups. MS can also construct various objects that it can prove satisfies that theory.
These axioms and proofs and theorems that MS constructs are all objects within MS itself. In contrast, when you define something in MS (and MS is a first-order theory), you can think of it as adding new axioms to MS itself!
Try not to get confused. MS is a first-order theory that can talk and reason about other first-order theories. There are 2 levels, the object level, which is where every mathematical object resides, and the meta level, which is where your definitions in MS reside.
There is one aspect of "definitions" that is not exactly asked in your question, but is relevant to mathematics. There are actually two kinds of completely formal definitions, arising from two separate mechanisms:
$
\def\nn{\mathbb{N}}
$
Definition by existential instantiation: When we have an ...
I'll be away for quite a while. Post your questions and I'll get back to them later.
@famesyasd I haven't forgotten about your this question about partial functions with a dedicate error value. =)
but even if one manages to proof that there is at least one proof by negation this is not enough. We need to make sure that what's being negated is the original statement.
prove*
alright, I can't think properly right now, I'm well past time when I should go to sleep, so I'll go to sleep now.
@famesyasd - My thought was to actually formulate an argument by contradiction; using coherent proofs as a sort of benchmark for "very positive reasoning" to show that there is no coherent proof of "sqrt 2 is not rational". That wouldn't settle the whole question, but if that line of thought worked it would tell you that any such proof must depend on a small number of other logical rules.
@user21820 may have something cleverer in mind, but that's what my thinking was.
@famesyasd @MaliceVidrine: When I thought about ¬intro again, I realized that the answer is quite trivial. If you think of the parse tree of each statement, you can see that there is no way to get "¬Q" anywhere in the parse tree unless you already have it in one of the axioms or use ¬intro on "Q ⊢ ⊥" at some point.
Note that we could have used ¬¬elim on "¬¬¬Q" to get "¬Q", but we can exclude such higher negations by induction. Namely, if we never use ¬intro then ¬¬elim is the only way to get "¬Q" in the parse tree of some deduced statement, so you need to have deduced "¬¬¬Q" earlier, and by induction you need an infinite sequence of odd-negations of Q being deduced earlier, which is impossible.
Actually, it's simpler than what I just said. Just consider the first deduced statement in the proof that has "¬Q" inside its parse tree. The only way it could have gotten there is via an axiom or ¬intro.
In the system where you replace DNE by LEM+EX, then using this simple analysis we're only able to conclude that either ¬intro or LEM or EX must be used somewhere in the proof.
The second explanation is much cleaner. You think of each deduced statement in the proof in terms of its parse tree. So for example "¬Q∧¬R" would contain "¬Q", while "¬(Q∨R)" would not. Then consider the very first deduced statement in the proof that contains "¬Q".
If "¬" is the root of the entire parse tree, then it could have gotten there by ¬intro. If not, then its child must have already been there in a previous deduced statement.
This applies to ¬¬elim as well, because "¬¬¬Q" does contain "¬Q".
The second explanation is much cleaner. You think of each deduced statement in the proof in terms of its parse tree. So for example "¬Q∧¬R" would contain "¬Q", while "¬(Q∨R)" would not. Then consider the very first deduced statement in the proof that contains "¬Q".
Each line in the Fitch-style proof is either a context header or a deduced statement. We only look at the parse trees of the deduced statements.
In this viewpoint, we consider a statement to contain "¬Q" iff its parse tree has a subtree that is exactly "¬Q".
There are other ways to express this, but I want you to think in terms of parse trees, because that's the correct way to think of inference rules.
" If not, then its child must have already been there in a previous deduced statement. "why is that? how it follows from that we take the very first deduded statement including "¬Q"?
Well, you just have to check the inference rules one by one. The key is that the inference rules only manipulate the outermost operations. So if "¬Q" is embedded somewhere inside the parse tree of the current statement, then it must have been there in some preceding statement already.
The main exceptions are if you just use an axiom, or if "¬" is at the root, in which case you could have gotten "¬Q" via ¬intro, which is the only way of 'introducing' "¬" with a new child.
So far this shows is that propositional logic cannot prove a non-axiom "¬Q" without using ¬intro. We still have some more work to show that PA cannot prove "¬∃x,y∈N ( x≠0 ∧ x·x = 2·y·y )" without using ¬intro, since PA comes with axioms. (CC @MaliceVidrine)
@AlessandroCodenotti: If you're curious, we're discussing how to show that PA as axiomatized here must use ¬intro in order to prove irrationality of sqrt(2), namely "¬∃x,y∈N ( x≠0 ∧ x·x = 2·y·y )".
When looking for occurrence of "¬Q", for each "⇒" we must ignore the left child subtree, namely for "A⇒B" we only look inside "B". Then I think the analysis works. ⇒intro works now. ⇒elim also works because we deduce "B" from "A" and "A⇒B". ∧intro/elim and ∨intro/elim work as before. Basically, ¬intro is the only rule that produces something from the left side of "⇒". (CC @MaliceVidrine)
Yay works now. When I think I can solve a problem, I must try to solve it. =)
Hmm I see a little problem, because "¬1<1" can be deduced from "1∈N" and "∀k∈N ( ¬k<k )" so we're going to have to do something to deal with the possibility that an induction axiom hides something that can be used to prove sqrt(2) irrationality. I'm quite sure it cannot, but I think you're right that we should leave this for now...
Well to evade the annoying thing about having to define a function-symbol on the whole world, even if it makes no sense for certain objects, like say division over the field axioms (where intuitively we treat division by zero as invalid), one might use the idea of partial-function-symbols instead of function-symbols. Partial-functions are like functions except on some inputs they don't have an output.
@famesyasd Without induction, you cannot prove the induction step without using ¬intro, because "m≠n" is "¬m=n" and we don't have that in any of the axioms.
So I doubt you can prove that without ¬intro. At least, my intuition says so.
Oh wait...
Okay forget it; "∨intro" never worked from the beginning.
I need to give up on this for now.
From "R" you can deduce "R∨¬Q". It's true that it's useless, but clearly we need something much more clever than what I've been trying.
As I said in the linked conversation, we can use some arbitrary output if the input is not in the domain. But presumably, you want the output to not be an object at all, is that right?
yes I want it to be something that would make sure that I don't want the input to be outside of the domain
something that I could actually feel that I'm using the premises that x in N or x in R
instead of like: suppose that we have a function f such that f = {(x,0) | x in R>0} and with garbage outputs I know that I could've actually proven not only that f(x) = 0 foralll x in R>0 but also f(x) = 0 forall x in R lol because I defined f(x) to be some of that garbage
Yea, the common definition of functions doesn't prevent garbage. For example, in ZFC a function f∈Func(S,T) is a subset of S×T, so we could elegantly define f(x) := Union( { y : y∈T ∧ ∃x∈S ( (x,y)∈f ) } ), but that would make f(x) = ∅ if x∉S, which you could consider as garbage since maybe f(x) = ∅ for some x∈S as well.
And similarly for defined function-symbols (via definitorial expansion).
So there are two ways I know to evade this problem. Both require a change to the underlying logic. The first is to have strict type-checking. Namely, you cannot even write "f(x)" unless f∈Func(S,T) and x∈S in that context.
This is closest to actual mathematical practice, and is compatible with the "Set Theory" I gave in my natural deduction rules post, even though I didn't say anything about it there.
This kind of strictness is not much different from my system's forbidding of undeclared variables. Most logic texts allow first-order formulae to have free variables, but there's no such thing in my system.
Similarly, here we're just forbidding writing "f(x)" unless it type-checks.
The second way is to even leave classical logic, and move to 3-valued logic, where we can have a non-object value "null" (or "undefined"). This is the direct implementation of the idea of partial-functions in the logic itself.
To handle this correctly, we have to decide what to do with equality. If we want to be able to use equality inside the definition of a function, then we cannot use that same equality for expressing "f(x) is null".
My preference is to keep "=" for equality between objects, and use "≡" for equivalence between expressions (that may refer to objects or may be null).
In that setting, we can stipulate that if f∈Func(S,T) and x∉S then f(x)≡null.
We can also stipulate that if f∈Func(S,T) and x∈obj then ( f(x)∈T ∨ (f(x)≡null) ).
But this approach doesn't make all problems go away. If S has boolean membership, then if f∈Func(S,T) and x∈obj and f(x)≡null then you can conclude that x∉S. But if you don't know that S has boolean membership (remember we're in 3-valued world now) then we cannot conclude that. So what you want may not be achievable, depending on what other things you want.
@user21820 Looking through these posts, I don't think they are very beginner-friendly. They presume more knowledge / familiarity with certain jargon up-front and are simply going to whoosh over everyone's heads, and I say this as someone who's already familiar with propositional logic!
