Mathbox for Frédéric Liné < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-ded Unicode version

Definition df-ded 25838
 Description: Definition of a deductive system. Lambeck and Scott. Introduction to higher order categorical logic. p. 47. 1986. Unformally we can say a deductive system is a directed multi graph where for each object a specific morphism called identity of the object exists and where for some pairs of morphisms the composite exists. Deductive system are named so because morphisms may be interpreted as logical deductions, objects as sets of formulas and compositions as inferences. (Contributed by FL, 24-Oct-2007.)
Assertion
Ref Expression
df-ded
Distinct variable group:   ,,,,,,,

Detailed syntax breakdown of Definition df-ded
StepHypRef Expression
1 cded 25837 . 2
2 vx . . . . . . . . . 10
32cv 1631 . . . . . . . . 9
4 vd . . . . . . . . . . . 12
54cv 1631 . . . . . . . . . . 11
6 vc . . . . . . . . . . . 12
76cv 1631 . . . . . . . . . . 11
85, 7cop 3656 . . . . . . . . . 10
9 vj . . . . . . . . . . . 12
109cv 1631 . . . . . . . . . . 11
11 vr . . . . . . . . . . . 12
1211cv 1631 . . . . . . . . . . 11
1310, 12cop 3656 . . . . . . . . . 10
148, 13cop 3656 . . . . . . . . 9
153, 14wceq 1632 . . . . . . . 8
16 calg 25814 . . . . . . . . . . 11
1714, 16wcel 1696 . . . . . . . . . 10
18 va . . . . . . . . . . . . . . . 16
1918cv 1631 . . . . . . . . . . . . . . 15
2019, 10cfv 5271 . . . . . . . . . . . . . 14
2120, 5cfv 5271 . . . . . . . . . . . . 13
2221, 19wceq 1632 . . . . . . . . . . . 12
2320, 7cfv 5271 . . . . . . . . . . . . 13
2423, 19wceq 1632 . . . . . . . . . . . 12
2522, 24wa 358 . . . . . . . . . . 11
2610cdm 4705 . . . . . . . . . . 11
2725, 18, 26wral 2556 . . . . . . . . . 10
28 vg . . . . . . . . . . . . . . . 16
2928cv 1631 . . . . . . . . . . . . . . 15
30 vf . . . . . . . . . . . . . . . 16
3130cv 1631 . . . . . . . . . . . . . . 15
3229, 31cop 3656 . . . . . . . . . . . . . 14
3312cdm 4705 . . . . . . . . . . . . . 14
3432, 33wcel 1696 . . . . . . . . . . . . 13
3529, 5cfv 5271 . . . . . . . . . . . . . 14
3631, 7cfv 5271 . . . . . . . . . . . . . 14
3735, 36wceq 1632 . . . . . . . . . . . . 13
3834, 37wb 176 . . . . . . . . . . . 12
395cdm 4705 . . . . . . . . . . . 12
4038, 28, 39wral 2556 . . . . . . . . . . 11
4140, 30, 39wral 2556 . . . . . . . . . 10
4217, 27, 41w3a 934 . . . . . . . . 9
4329, 31, 12co 5874 . . . . . . . . . . . . . . 15
4443, 5cfv 5271 . . . . . . . . . . . . . 14
4531, 5cfv 5271 . . . . . . . . . . . . . 14
4644, 45wceq 1632 . . . . . . . . . . . . 13
4737, 46wi 4 . . . . . . . . . . . 12
4847, 28, 39wral 2556 . . . . . . . . . . 11
4948, 30, 39wral 2556 . . . . . . . . . 10
5043, 7cfv 5271 . . . . . . . . . . . . . 14
5129, 7cfv 5271 . . . . . . . . . . . . . 14
5250, 51wceq 1632 . . . . . . . . . . . . 13
5337, 52wi 4 . . . . . . . . . . . 12
5453, 28, 39wral 2556 . . . . . . . . . . 11
5554, 30, 39wral 2556 . . . . . . . . . 10
5649, 55wa 358 . . . . . . . . 9
5742, 56wa 358 . . . . . . . 8
5815, 57wa 358 . . . . . . 7
5958, 11wex 1531 . . . . . 6
6059, 9wex 1531 . . . . 5
6160, 6wex 1531 . . . 4
6261, 4wex 1531 . . 3
6362, 2cab 2282 . 2
641, 63wceq 1632 1
 Colors of variables: wff set class This definition is referenced by:  isded  25839  dedi  25840  strded  25842
 Copyright terms: Public domain W3C validator