TWiki> Mizar Web>CollaborativeManual>ManualPl>ManualPlAbstract>ManualPlSchemes>ManualPlFormula (2012-01-29, GrzegorzBancerek)EditAttach

Formuła

start

Formuła jest zbudowana z formuł atomowych połączonych za pomocą spójników logicznych: negacji not, koniunkcji &, alternatywy or, implikacji implies i równoważności iff oraz za pomocą kwantyfikatorów: ogólnego for i egzystencjalnego ex.

Formuła Logika
not α ¬ α
α & β α ∧ β
α or β α ∨ β
α implies β α ⇒ β
α iff β α ⇔ β
for x being Θ holds β ∀x:Θ β
for x being Θ st α holds β ∀x:Θ (α⇒β)
ex x being Θ st α ∃x:Θ α

Silła wiązania spójników jest następująca: najsilniej wiąże not. potem &, or, implies i iff, for i ex. Jeśli nie ma nawiasów to przyjęte jest grupowanie do lewej: α & β & γ rozumiane jest jako (α & β) & γ Wielokrotne użycie spójnika implies lub iff wymaga wstawienia nawiasów: (α implies β) iff γ. lub α implies (β iff γ).

Jeśli w formule ogólnej po holds stoi kwantyfikator, to holds można pominąć: for x being Θ st α holds ex y being Θ st β można zpisać tak for x being Θ st α ex y being Θ st β.

Zobacz twiedzenie, schemet, definiens?, formła dodatkowa?.

WebForm
TopicClassification Select one...
ProjectGroup?

ImplementationDate? N/A
Edit | Attach | Print version | History: r8 < r7 < r6 < r5 < r4 | Backlinks | Raw View | Raw edit | More topic actions
Topic revision: r8 - 2012-01-29 - 17:48:36 - GrzegorzBancerek
Mizar.ManualPlFormula moved from Mizar.ManualOlFormula on 2012-01-20 - 09:37 by GrzegorzBancerek - put it back
 
Mizar TWiki
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback