Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
[Official] Assignment 7
posted
I have several questions:
7.1. Induction
- Does this mean recursively defining the function C?
- Is it possible that there are predicats in the formula (because you just wrote term/formula)? Should we define how to handle predicats as well?
7.2 First-Order Semantics
- We are not given an interpretation. So how should we actually say anything about things like I(+)?
- When we transform the derived connectors (=>, OR) to the basic connectors (AND, NOT) first, can we simply dispose things like NOT NOT?
- We don’t know anything about the domain of the individuals. Should we keep it general, when we write about interpreting the variables?
Thanks! 
Hello,
we have also a question regarding
Problem 7.3. Natural Deduction
Slide 405 in slides.pdf (20-Jan-2021 09:56) says:
If i am not wrong this means: If X is not free in the assumption(s) that lead to A, we can conclude ∀X.A.
But Fitch-Kalkül – Wikipedia says about ∀I:
That would seem to contradict the definiton above.
It’s nothing new that wikipedia sometimes isn’t correct (and me anyway ;)), but what exactly is true now? If wikipedia is wrong with this one, the first step for 7.3.1 would be impossible in my opinion, as we somehow have to assume the antecedent in the implication in any time of the proof, where X is free in the antecedent. Confusion is real !
Please help clarifying this.
Thanks in advance
But thats exactly what Wikipedia said. I don’t see why the script contradicts Wikipedia here anyway.
@Florian Rabe: Would you please answer all questions as i am not the only one who got some!
I am also not quite satisfied with your short answer… Maybe i should rephrase it and take an example: Let’s say i have (Example 13.3.2 in slides.pdf):
… [¬P(X)]^2
…
P(X)
------------- ∀I
∀X.P(X)
Obviously X is free in assumption 2, however we still make a forall introduction, where Definition 13.3.1 mentions: [quote]A does not depend on any hypothesis in which X is free
[/quote]
Forall Introduction
Maybe I can help:
The difference between the wikipedia version and ours is that these are two different notation systems that refer to two different things with their “free variable”
Let’s first go over the sequent-notation
Γ |- A ¬ (X ∈ free(Γ))
--------------------------------- ∀I
Γ |- ∀X.A
What does this mean? Well, before we can introduce a forall, we need to make sure we don’t have any further assumptions about the variable X:
{P(X)} |- A ¬ (X ∈ free({P(X)}))
--------------------------------- ∀I
Γ |- ∀X.A
This would be an illegal derivation because X is a free variable in the context Γ. In practice the ¬ (X ∈ free(Γ)) just means that you aren’t allowed to have any assumptions that already deal with the variable you want to write a forall around:
If you already knew something about the X (i.e. that P(X) holds…) then your choice of X wasn’t completely arbitrary and therefore we cannot conclude that it actually holds for an arbitrary X.
Now, why does Wikipedia say something different?
The article you have linked talks about Fitch-style proofs. Fitch proofs is a special way of writing down natural deduction proofs that doesn’t rely on Sequents, but rather on nested proof contexts. In this notation, you just have to make sure that the X doesn’t appear outside the context (which if you apply the rules never happens…). In fitch-notation, it is sufficient to say “free variables can get a forall” because you assumed them to be free in the scope of the subproof (i.e. the only way to introduce a variable is to make sure it was never used before). I attached a small Fitch-style proof I made for ∀X.P(X) → ∃ X. P(X)
This obviously doesn’t have a forall introduction (I couldn’t find a small theorem to show forall in…) but it should get the idea across
Attachment:
smallproof.png: https://fsi.cs.fau.de/unb-attachments/post_165974/smallproof.png
1 „Gefällt mir“
Assumption 2 is not active at this point anymore. It ends after the ¬I so your only assumption that is active is Ass1 and there X is not free so everything is fine.
In sequent style Γ is the set of active assumptions.
That is not correct. If you can show P(X) with X not free in any assumptions you made to show this, you can open a subproof with x not free in the assumption as well and still say ∀x.p(x). Althoug I am not sure if you need to do that at any point. Probably you can just reformulate your proof then and just write ∀x.p(x) outside the new subproof.
1 „Gefällt mir“
Thanks KMB and Comonade for your answers, i really appreciate it !
One general, probably trivial, question i have on Natural Deduction is:
If we have to proof any formula A and we can assume anything, why don’t just assume ¬X and X and make a FI and afterwards a FE to conclude anything we like, for example A. We would have shown that A was derived from our assumptions and could be happy… What is wrong with this thought? Does Natural Deduction dependent on “finding good assumptions”?
The issue is that it only holds under the contradictory assumptions X and not X, while the point is to prove something in general.
Solutions posted
Wikipedia had
X = ungerade |- ∀X.(X = ungerade)
That is different from
X = ungerade
∀X.(X = ungerade)
Only the latter is how forall introduction works.
Which question did I miss?
X is not free in an assumption anymore when ∀I is applied because that assumption was discharged in between.
(I find these issues get clearer in sequent notation.)
Thanks, i think i understood it now.
There was luzi57 asking some questions before me. ([Official] Assignment 7 - Künstliche Intelligenz - FSI Informatik Forum).
Sorry, I overlooked this question.
For 7.1, the answers were yes and yes.
For 7.2, you were supposed to use an arbitrary interpretation I, same for the domain of the individuals.
Regarding derived connectors, technically, you should prove a lemma that handles the disposing. Then you can apply it whenever you like.