rekursive funksjoner

[Carls]

Jeg har problem med denne oppgaven.


La Hyp(D) være en rekursiv funksjon fra utledninger til mengder av formler, slik at Hyp(D) er nøyaktig de ̊apne antakelsene i D. Du kan anta at vi alltid lukker alle de antakelsene vi kan lukke.
For eksempel, for ∧I: Vi starter med D1 φ og D2 ψ, og setter sammen til utledningen (D1φ D2ψ )/(φ∧ψ ). Da har vi
Hyp(D1φ D2ψ )/(φ∧ψ ) = Hyp(D1φ) ∪ Hyp (D2ψ)

Gi hele definisjonen for Hyp(D).

[peterbb]

Hvor er du stuck?


Hvis vi ser på et eksempel, vet du hva svaret skal være? Hva er f.eks. [tex]Hyp\left(\begin{array}{c} \underline{[A] \quad B} \\ A \land B \\ \overline{A \supset (A \land B)} \end{array}\right)[/tex] er?


Vet du f.eks. hvilke tilfeller du må ha med? Du skrev selv et tilfelle:
[tex]Hyp\left( \frac{ \overset{\mathcal{D}_1}{\phi} \quad \overset{\mathcal{D}_2}{ \varphi}}{\phi \land \varphi}\right) = Hyp\left(\overset{\mathcal{D}_1 }{ \phi}\right) \cup Hyp\left(\overset{\mathcal{D}_2}{ \varphi}\right)[/tex]

Hva er de andre tilfellene? For eksempel, her er tilfellet for den første [tex]\land[/tex]-eliminasjonsregelen:
[tex]Hyp\left(\frac{ \overset{ \mathcal{D}}{\phi \land \varphi} }{\phi} \right) = \cdots[/tex]

Og regelen for impliasjon introduksjon.
[tex]Hyp\left( \frac{ \begin{array}{c} [A]\\ \mathcal{D} \\ B \end{array} }{ A \supset B } \right) = \cdots[/tex]

Du kommer til å trenge et tilfelle for hver regel.

- Peter

[Carls]

Jeg kommet fram til:

Hyp((F->G F)/G) = Hyp(F->G) U Hyp(F)

basistilfelle: Hyp(phi)= { phi }

hyp((⊥/ phi) ⊥)=Hyp(⊥)
Hyp((F∧G)/F ∧ E)=Hyp(F∧G)
Hyp((F∧G)/G ∧E)= Hyp(F∧G)
Hyp(psi/(phi -> psi)->I)=Hyp(psi D psi/{ psi })
Γ = Γ U { phi }/{ phi }

Nå sitter jeg fast.

-Carls

Hvor er du stuck?


Hvis vi ser på et eksempel, vet du hva svaret skal være? Hva er f.eks. [tex]Hyp\left(\begin{array}{c} \underline{[A] \quad B} \\ A \land B \\ \overline{A \supset (A \land B)} \end{array}\right)[/tex] er?


Vet du f.eks. hvilke tilfeller du må ha med? Du skrev selv et tilfelle:
[tex]Hyp\left( \frac{ \overset{\mathcal{D}_1}{\phi} \quad \overset{\mathcal{D}_2}{ \varphi}}{\phi \land \varphi}\right) = Hyp\left(\overset{\mathcal{D}_1 }{ \phi}\right) \cup Hyp\left(\overset{\mathcal{D}_2}{ \varphi}\right)[/tex]

Hva er de andre tilfellene? For eksempel, her er tilfellet for den første [tex]\land[/tex]-eliminasjonsregelen:
[tex]Hyp\left(\frac{ \overset{ \mathcal{D}}{\phi \land \varphi} }{\phi} \right) = \cdots[/tex]

Og regelen for impliasjon introduksjon.
[tex]Hyp\left( \frac{ \begin{array}{c} [A]\\ \mathcal{D} \\ B \end{array} }{ A \supset B } \right) = \cdots[/tex]

Du kommer til å trenge et tilfelle for hver regel.

- Peter

[peterbb]

Jeg kommet fram til:

Hyp((F->G F)/G) = Hyp(F->G) U Hyp(F)

basistilfelle: Hyp(phi)= { phi }

hyp((⊥/ phi) ⊥)=Hyp(⊥)
Hyp((F∧G)/F ∧ E)=Hyp(F∧G)
Hyp((F∧G)/G ∧E)= Hyp(F∧G)
Hyp(psi/(phi -> psi)->I)=Hyp(psi D psi/{ psi })
Γ = Γ U { phi }/{ phi }

Synes det ser bra ut. Husk at det er viktig å skille mellom bevistrærne og formelene, så husk å bruke en passende notasjon, f.eks.:
[tex]Hyp\left(\frac{ \overset{\mathcal{D}_0}{F \to G} \quad \overset{\mathcal{D}_1}{F} }{ G }\right) = Hyp\left( \overset{\mathcal{D}_0}{F\to G} \right) \cup Hyp\left( \overset{\mathcal{D}_1}{F} \right)[/tex].
Tilfellet ditt for pil-introduksjon er ikke helt riktig. Hvis jeg tolker det du har skrevet riktig, så har du noe sånt som:
[tex]Hyp\left( \frac{ \overset{\mathcal{D}}{\psi} }{ \varphi \to \psi } \right) = Hyp\left( \overset{\mathcal{D}}{\psi} \setminus \{ \psi \} \right)[/tex]
Et problem her er at du tar mengde-differansen mellom et bevistre og en mengde, noe som ikke gir mening. Du ønsker nok heller at det er på følgende form: [tex]Hyp\left( \ldots \right) \setminus \{ \ldots \}[/tex] siden [tex]Hyp[/tex] gir deg en mengde med antagelser, også ønsker du å fjerne noen av disse.

Videre, så fjerner du her [tex]\psi[/tex], noe som er feil ting å fjerne. Hvilke antagelser er det som kan fjernes i et pil-intro bevis?

Ellers ser det bra ut. Jeg forstår dog ikke hvorfor du har skrevet [tex]\Gamma = \Gamma \cup \{ \phi \} \setminus \{\phi \}[/tex].

Nå sitter jeg fast.

Jeg ser ikke hvor du står fast. Er det et konkret tilfelle du ikke får til? Resten av tilfellen følger samme mønster som de andre.

- Peter

[Carls]

Jeg skjønner ikke helt hva er neste steg som må gjøres?

Jeg kommet fram til:

Hyp((F->G F)/G) = Hyp(F->G) U Hyp(F)

basistilfelle: Hyp(phi)= { phi }

hyp((⊥/ phi) ⊥)=Hyp(⊥)
Hyp((F∧G)/F ∧ E)=Hyp(F∧G)
Hyp((F∧G)/G ∧E)= Hyp(F∧G)
Hyp(psi/(phi -> psi)->I)=Hyp(psi D psi/{ psi })
Γ = Γ U { phi }/{ phi }

Synes det ser bra ut. Husk at det er viktig å skille mellom bevistrærne og formelene, så husk å bruke en passende notasjon, f.eks.:
[tex]Hyp\left(\frac{ \overset{\mathcal{D}_0}{F \to G} \quad \overset{\mathcal{D}_1}{F} }{ G }\right) = Hyp\left( \overset{\mathcal{D}_0}{F\to G} \right) \cup Hyp\left( \overset{\mathcal{D}_1}{F} \right)[/tex].
Tilfellet ditt for pil-introduksjon er ikke helt riktig. Hvis jeg tolker det du har skrevet riktig, så har du noe sånt som:
[tex]Hyp\left( \frac{ \overset{\mathcal{D}}{\psi} }{ \varphi \to \psi } \right) = Hyp\left( \overset{\mathcal{D}}{\psi} \setminus \{ \psi \} \right)[/tex]
Et problem her er at du tar mengde-differansen mellom et bevistre og en mengde, noe som ikke gir mening. Du ønsker nok heller at det er på følgende form: [tex]Hyp\left( \ldots \right) \setminus \{ \ldots \}[/tex] siden [tex]Hyp[/tex] gir deg en mengde med antagelser, også ønsker du å fjerne noen av disse.

Videre, så fjerner du her [tex]\psi[/tex], noe som er feil ting å fjerne. Hvilke antagelser er det som kan fjernes i et pil-intro bevis?

Ellers ser det bra ut. Jeg forstår dog ikke hvorfor du har skrevet [tex]\Gamma = \Gamma \cup \{ \phi \} \setminus \{\phi \}[/tex].

Nå sitter jeg fast.

Jeg ser ikke hvor du står fast. Er det et konkret tilfelle du ikke får til? Resten av tilfellen følger samme mønster som de andre.

- Peter

[peterbb]

Hvis du har definert funksjonen for hvert tilfelle, så er du ferdig.

[Calrs]

Hva mener du med å ha definert funksjonen for hvert tilfelle?

Hvis du har definert funksjonen for hvert tilfelle, så er du ferdig.

[peterbb]

Et tilfelle er [tex]Hyp\left( \frac{ \overset{\mathcal{D}_0}{F} \quad \overset{\mathcal{D}_1}{G} }{ F \land G }\land{}i \right) = Hyp\left( \overset{\mathcal{D}_0}{F}\right) \cup Hyp\left( \overset{\mathcal{D}_1}{G} \right)[/tex]. Du trenger et tilfelle for hver regel i bevissystemet.

[Carls]

Men er ikke disse tilfellene har jeg skrevet helt oppe?

DVS:
""
Hyp((F->G F)/G) = Hyp(F->G) U Hyp(F)

basistilfelle: Hyp(phi)= { phi }

hyp((⊥/ phi) ⊥)=Hyp(⊥)
Hyp((F∧G)/F ∧ E)=Hyp(F∧G)
Hyp((F∧G)/G ∧E)= Hyp(F∧G)
Hyp(psi/(phi -> psi)->I)=Hyp((psi D )/{ psi })
Γ = Γ U { phi }/{ phi }
""

Et tilfelle er [tex]Hyp\left( \frac{ \overset{\mathcal{D}_0}{F} \quad \overset{\mathcal{D}_1}{G} }{ F \land G }\land{}i \right) = Hyp\left( \overset{\mathcal{D}_0}{F}\right) \cup Hyp\left( \overset{\mathcal{D}_1}{G} \right)[/tex]. Du trenger et tilfelle for hver regel i bevissystemet.

[peterbb]

Men er ikke disse tilfellene har jeg skrevet helt oppe?

DVS:
""
Hyp((F->G F)/G) = Hyp(F->G) U Hyp(F)

basistilfelle: Hyp(phi)= { phi }

hyp((⊥/ phi) ⊥)=Hyp(⊥)
Hyp((F∧G)/F ∧ E)=Hyp(F∧G)
Hyp((F∧G)/G ∧E)= Hyp(F∧G)
Hyp(psi/(phi -> psi)->I)=Hyp((psi D )/{ psi })
Γ = Γ U { phi }/{ phi }
""

Jo, men dere har vel flere regler? Sånn som [tex]\lor[/tex]-introduksjon og eliminasjon, og kanskje til og med en form for RAA-regel. Altså, du må også beskrive hva hyp-funksjonen gjør i disse tilfellene.