Argument index

Master / Vertiefung Logikbasierte Wissensrepräsentation
1

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.

2

Argument index
hello,
please can anyone tell me if this is right ?

andEliminationLeft : {A,B} ⊦ A ∧ B ⟶ ⊦ A ❘ # andEl 3 ❙ // argument 3 is A ?

andEliminationRight: {A,B} ⊦ A ∧ B ⟶ ⊦ B ❘ # andEr 3 ❙ // argument 3 is B ?

andIntroduction : {A,B} ⊦ A ⟶ ⊦ B ⟶ ⊦ A ∧ B ❘ # andI 3 4 ❙ // argument 3 is B and argument 4 is A ∧ B ?

implicationElim : {A,B} ⊦ A ⟹ B ⟶ ⊦ A ⟶ ⊦ B ❘ # impE 3 4 ❙ // argument 3 is A and argument 4 is B ?

implicationIntro : {A,B} (⊦ A ⟶ ⊦ B) ⟶ ⊦ (A ⟹ B) ❘ # impI 3 ❙ // argument 3 is (A ⟹ B)

thanks :slight_smile:

3

Oh the last thing i forgot.

why did we need curly braces again e.g {A,B}?

4

None of these are right, I’m sorry to say.

“{A,B} ⊦ A ∧ B ⟶ ⊦ A” is a ternary function taking three arguments; One called A (of type prop), one called B (of type prop), and one unnamed one of type ⊦ A ∧ B.

Hence: argument 1 is A, argument 2 is B and argument 3 is some element of type ⊦ A ∧ B.

It might be more comfortable to imagine the syntax being instead:
(A : prop) ⟶ (B : prop) ⟶ ⊦ A ∧ B ⟶ ⊦ A

1 „Gefällt mir“
5

Thanks you very much. this is now much clearer :smiley:

6

For the same reason we need the square brackets :wink:

Where „[x:A] t(x)“ says „the function taking an x:A as argument and returning t(x)“, the expression „{x:A} T(x)“ says „the TYPE of all functions taking an x:A as argument and returning an element of TYPE T(x)“.

So if t(x) has type T(x), then the type of [x:A]t(x) is {x:A}T(x).

And if T does not actually depend on x at all, then {x:A}T is just the type A->T. In fact, the simple function type A->B is really just an abbreviation for {_:A}B

2 „Gefällt mir“