# Argument index

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.

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

Oh the last thing i forgot.

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

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 Like

Thanks you very much. this is now much clearer

For the same reason we need the square brackets

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 Likes