Схемы аксиом с описанием и поиск теорий, в которых доказуема выбранная формула

На этой странице Вы можете выбрать формулу и получить перечень некоторых теорий, в которых данная формула доказуема.

	¬¬AA	снятие двойного отрицания
	¬(SaP&SaP´)
	¬(SaS´ & S´aS)
	¬i
	¬A(AB)	закон противоречия
	¬SaP
	¬SaPSoP
	¬SaS´
	¬SeP
	¬SePSiP
	¬SeS
	¬SiP
	¬SiPSeP
	¬SiS´
	¬SiS  SaP
	¬SoP
	¬f	закон непротиворечия
	þA A	формализация аксиомы Спинозы: Idea vera debet cum suo ideato convenire (Истинная идея должна быть согласна с своим объектом)
	(¬SaP & SiS)  SoP
	(¬SiP & SiS)  SeP
	((AB)&(BA))(AB)
	(A&B)A	исключение конъюнкции
	(A&B)B	исключение конъюнкции
	(AB)((AB)&(BA))
	(A((BB)A))(((AB)B)((BA)A))
	(A((BC)D))((BC)(AD))
	(A(AB))(AB)
	(A(BC))((AB)(AC))	самодистрибутивность импликации
	(A(BC))(B(AC))
	(AA)(((((AB)B)A)C)(((((BA)A)B)C)C))
	(AB)((A¬B)¬A)
	(AB)(C(AB))
	(AC)((BC)((AB)C))
	(BC)((AB)(AC))
	(MS & MP)  M (SP)
	(MaP & MiS)  SiP
	(MaS & MaP)  Ma(SP)
	(MeP&SaM)SaP´
	(MeP&SiM)SiP´
	(PP´)S
	(SM & MP)  SP
	(SM & MaP)  SP
	(SP & PP)  PS
	(S(PM))((SP)(SM))
	(SP)´(S´P´)
	(SP)eM  (MS)eP
	(SP)iM  SiP
	(SM & MP)  SP
	(SM & PM)  (SP)M
	(SP & PS)  S=P
	(SM & MP) SP	транзитивность строгого включения
	(S=M & M=P)  S=P
	(SaM & MaP)  SaP	модус barbara
	(SaM & MeP)  SeP	модус celarent
	(SaP  SiP)  (PaS  PiS)
	(SaP  SiP)  SaS
	(SaP  StP)  SaS
	(SaP  StP)  (PaS  PtS)
	(SaS&¬PaP)SeP
	(SaS & SeP´)  SaP
	(SeM & MeP)  SaP
	(SeP & PiP & PoP)  SeS
	(SiM & MaP)  SiP
	(SiM & MiP)  SiP
	(SoP & SiS)  SiP´
	(SuM & MaP)  SuP
	(SuM & MaP)  SuP
	(a<b & b<c) a<c	транзитивность строгого порядка
	(a=b & b=c) a=c	транзитивность равенства
	(vaS & vaP)  SiP
	(vS & SaP)  vP
	(vS & vP)  SiP
	(vaM & MaP)  vaP
	(A&AB) (B&BA)	модальная аксиома 3
	(AB)(AB)	модальная аксиома K
	A	модальная аксиома V, или Ver
	A A	модальная аксиома 4
	AA	модальная аксиома D
	AA	модальная аксиома T
	(A&B) (A B)	модальная аксиома 2
	A ¬¬A	связь сильной и слабой модальностей
	A A	модальная аксиома Triv
	A A	модальная аксиома Tc
	AA	модальная аксиома 5
	P
	x(yCxy zTzx) & x(yTxy zCzx)	формализация аксиомы Спинозы: Из данной определенной причины необходимо вытекает действие, и наоборот, – если нет никакой определенной причины, невозможно, чтобы последовало действие
	x(A B) (A xB), если A не содержит свободных вхождений x
	x(Cxx Nx)	формализация определения Спинозы: Per causam sui intelligo id, cujus essentia involvit existentiam; sive id, cujus natura non potest concipi nisi existens (Под причиною самого себя я разумею то, сущность чего заключает в себе существование, иными словами, то, чья природа может быть представляема не иначе: как существующею)
	x(Dxx Cxx)	экспликация пресуппозиции Спинозы: x зависит от самого себя е.т.е. x - причина самого себя
	x(Ex Nx)	формализация определения Спинозы: Под вечностью я понимаю самое существование, поскольку оно представляется необходимо вытекающим из простого определения вечной вещи
	x(Gx (Sx & Hx))	формализация определения Спинозы: Per Deum intelligo ens absolute infinum, hoc est, substantiam constantem infinitis attributus, quorum unumquodque aeter-nam, et infinitam essentiam exprimit (Под Богом я разумею существо абсолютно бесконечное, т.е. субстанцию, состоящую из бесконечно многих атрибутов, из которых каждый выражает вечную и бесконечную сущность)
	x(Ixx y(¬x=y & Ixy))	формализация аксиомы Спинозы: Все, что существует, существует или само в себе, или в чем-то другом
	x(Kx y(Kxy & Lyx & ¬x=y))	формализация определения Спинозы: Ea res dicitur in suo genere finita, quae alia ejusdem narurae terminari potest. Ex. gr. corpus dicitur finitum, quia aliud semper majus concipimus. Sic cogitatio alia cogitatione terminatur. At corpus non terminatur cogitatine, nec cogitatio corpore (Конечною в своем роде называется такая вещь, которая может быть ограничена другой вещью той же природы. Так, например, тело называется конечным, потому что мы всегда представляем другое тело, еще большее. Точно так же мысль ограничивается другой мыслью. Но тело не ограничивается мыслью, и мысль не ограничивается телом)
	x(Nx y(Eyx z(Azy u(z=u))))	формализация аксиомы Спинозы: Сущность всего того, что может быть представляемо не существующим, не заключает в себе существования
	x(Qx ¬yLyx)	экспликация пресуппозиции Спинозы: Что-либо является свободным е.т.е. его ничто не ограничивает
	x(Qx (Nx & Cxx))	формализация определения Спинозы: Свободной называется такая вещь, которая существует по одной только необходимости своей собственной природы и определяется к действию только сама собой. Необходимой же или, лучше сказать, принужденной называется такая, которая чем-либо иным определяется к существованию и действию по известному и определенному образу
	x(Sx Dxx)	одна из трех аксиом, формализующих третее определение Спинозы: Per substantiam intelligo id, quod in se est, et per se concipitur: hoc est id, cujus conceptus non indiget conceptu alterius rei, a quo formari debeat (Под субстанцией я разумею то, что существует само в себе и представляется само через себя, т.е. то, представление чего не нуждается в представлении другой вещи, из которой оно должно было бы образоваться)
	x(Sx Ixx)	одна из трех аксиом, формализующих третее определение Спинозы: Per substantiam intelligo id, quod in se est, et per se concipitur: hoc est id, cujus conceptus non indiget conceptu alterius rei, a quo formari debeat (Под субстанцией я разумею то, что существует само в себе и представляется само через себя, т.е. то, представление чего не нуждается в представлении другой вещи, из которой оно должно было бы образоваться)
	x(Sx ¬ y (Dxy & ¬y=x))	одна из трех аксиом, формализующих третее определение Спинозы: Per substantiam intelligo id, quod in se est, et per se concipitur: hoc est id, cujus conceptus non indiget conceptu alterius rei, a quo formari debeat (Под субстанцией я разумею то, что существует само в себе и представляется само через себя, т.е. то, представление чего не нуждается в представлении другой вещи, из которой оно должно было бы образоваться)
	x(x=x)	рефлексивность равенства
	xy(Sx Ayx)	одна из двух аксиом, формализующих четвертое определение Спинозы: Per attributum intelligo id, quod intellectus de substantia percipit, tanquam ejusdem essentiam constituens (Под атрибутом я разумею то, что ум представляет в субстанции как составляющее ее сущность)
	xy(¬zWxyz (v(Uvx & ¬Uvy) & v(Uvy & ¬Uvx) & ¬Dxy & ¬Dyx))	формализация аксиомы Спинозы: Вещи, не имеющие между собой ничего общего, не могут быть и познаваемы одна через другую; иными словами - представление одной не заключает в себе представления другой
	xy((¬x=y & ¬Dxy) Dxx)	формализация аксиомы Спинозы: Что не может быть представляемо через другое, должно быть представляемо само через себя
	xy((¬x=y & Dxy) Pyx)	экспликация пресуппозиции Спинозы: Если x и y различны и x зависит от y, то y первее x
	xy((Dxy Dyx) wWxyw)	экспликация пресуппозиции Спинозы: x зависит от y или y зависит от x е.т.е. x и y имеют что-либо общее
	xy(Axy (Sy & Exy))	одна из двух аксиом, формализующих четвертое определение Спинозы: Per attributum intelligo id, quod intellectus de substantia percipit, tanquam ejusdem essentiam constituens (Под атрибутом я разумею то, что ум представляет в субстанции как составляющее ее сущность)
	xy(Cxy z(Uzy Uzx))	формализация аксиомы Спинозы: Знание действия зависит от знания причины и заключает в себе последнее
	xy(Mxy (Sy & Ixy & ¬x=y & Dxy))	формализация определения Спинозы: Per modum intelligo substantiae affectiones, sive id, quod in alio est, per quod etiam concipitur (Под модусом я разумею состояние субстанции, иными словами, то, что существует в другом и представляется через другое)
	xy(x<y ¬y<x)	антисимметричность строгого порядка
	xy(x=y ¬x<y)	несовместимость равенства и строгого порядка
	xy(x=y y=x)	симметричность равенства
	xyuv((Eux & Evy) (x=y u=v))	экспликация пресуппозиции Спинозы: Если u - сущность x и v - сущность y, то x=y е.т.е. u=v
	xyz(x<y & y<z x<z)	транзитивность строгого порядка
	xyz(x=y & y=z x=z)	транзитивность равенства
	xA(x) A(t), если не одна переменная из терма t не оказывается связанной в результате такой подстановки
	A xA	принцип обобщения (генерализация)
	A&¬A	противоречие
	A(AB)	введение дизъюнкции
	A(B(A&B))	введение конъюнкции
	A(BA)	закон утверждения консеквента
	A A	модальная аксиома B, Br
	AA	закон тождества
	B(AB)	введение дизъюнкции
	C((AB)(AB))
	MaSMaP
	Me(SP)´  (MeS´ & MeP´)
	Me(SP)  (MeS & MeP)
	P´´P
	PaP(SePPeS)
	S´´aPSaP
	S´´aS
	SP  SS
	SP  SaP
	SP (SP S=P)	определение нестрогого включения через равенство и строгое включение
	SP´  PS´
	SS	рефлексивность нестрогого включения
	SP ¬PS	антисимметричность строгого включения
	S=P ¬SP	несовместимость равенства и строгого включения
	S=P  P=S	симметричность равенства
	S=S	рефлексивность равенства
	SaP
	SaP PaP
	SaP SaS
	SaP´´SaP
	SaP´  (SeP & SiS)
	SaP  SeP  SiP
	SaP  SeP  StP
	SaP  (SeP´ & SiS)
	SaP  SeP´
	SaP  ¬SeP	контрарность высказываний типа A и E
	SaP  ¬SiP
	SaP  ¬StP
	SaP  (SaS & PaP)
	SaP  PaS
	SaP  SeP´
	SaP  SiP	закон подчинения
	SaP  SiS
	SaP  SqP
	SaPSiS
	SaP(SiP&SeP´)
	SaPP´aS´
	SaS	закон силлогистического тождества для A
	SaS´´
	SaS´SaP
	SaS  (SaP  SeP  SiP)
	SaS  (SaP  SeP  StP)
	SeM(PeM´SeP)
	SeM(PiMS´iP)
	SeP
	SeP ¬SiP	контрадикторность высказываний типа E и I
	SeP SaS
	SeP  (¬SiP & SiS)
	SeP  ¬SiP
	SeP  ¬StP
	SeP  PeS	закон обращения E
	SeS SaS
	SeS SaP
	SeS SeP
	SeS´
	SiP
	SiP  SiP´´
	SiP  (SP)aP
	SiP  (SP)aS
	SiP  PiS	закон обращения I
	SiP  SaP
	SiP  SiS
	SiPSaS
	SiP¬SeP
	SiPSaS
	SiS  S´iS´
	SiS  SqS
	SiS  SaS
	SiSSaU
	SoP  (¬SaP & SiS)
	SoP  ¬SaP	контрадикторность высказываний типа A и O
	SoP  ¬SaP
	SoP  PqP
	SoP  SiS
	SoP(SePSiP´)
	SoPSiP´
	SoS´
	SqP  ¬SuP
	SqP  SaS
	SqP  SqS
	SqS
	SuP  PuS
	a<b ¬b<a	антирефлексивность строгого порядка
	a=a	рефлексивность равенства
	a=b ¬a<b	несовместимость равенства и строгого порядка
	a=b b=a	симметричность равенства
	fA	закон противоречия
	t
	uS  PaS
	uS  SiS
	v´iv´
	vaw  wav
	vS  (vP  vP´)
	vS  vyS´
	vav
	veS  vaS´
	vyS  ¬vS
	vyS  vS´
	Схемы аксиом интуиционистской логики высказываний	введено для сокращения описания прикладных теорий, см. определение теории H
	Схемы аксиом классической логики высказываний	введено для сокращения описания прикладных теорий, см. определение теории TV
	Схемы аксиом классической логики предикатов	введено для сокращения описания прикладных теорий, см. определение теории QTV
	Схемы аксиом теории THcie+	введено для сокращения описания прикладных теорий. Существует описание только с правилами вывода. Для формулировки с аксиомами необходимы дальнейшие исследования.