論理 Mizar ⊥ contradiction ¬φ not φ φ ∧ ψ φ & ψ φ ∨ ψ φ or ψ φ ⇒ ψ φ implies ψ φ ⇔ ψ φ iff ψ ∃ x. ψ ex x st ψ ∀ x. ψ for x holds ψ ∀ x.(φ ⇒ ψ) for x st φ holds ψ nonは形容詞の否定、andとsuch thatはスクリプト言語のキーワード。

Mizarでは同義語はほとんどない。beとbeing, hence（従って）、hereby（これによって）が次の意味。 then + thus = hence thus + now = hereby 英語としてはthus（よって）とhence（従って）はたいして差はない。