Metamath について

Words near each other

・ Metal–ligand multiple bond
・ Metal–semiconductor junction
・ Metam sodium
・ Metamagical Themas
・ Metamagnetism
・ Metamagnusia slateri
・ Metamale
・ Metaman
・ Metamaterial
・ Metamaterial absorber
・ Metamaterial antenna
・ Metamaterial cloaking
・ Metamaterials (journal)
・ Metamaterials Handbook
・ Metamaterials surface antenna technology
・ Metamath
・ Metamathematics
・ Metamathics
・ Metamatic
・ Metamatic Records
・ MetaMatrix
・ MetaMaus
・ Metamec
・ Metamechanics
・ Metamecyna
・ Metamecyna flavoapicalis
・ Metamecyna uniformis
・ Metamecynopsis duodecimguttata
・ MetaMed
・ Metamedia

Dictionary Lists

mini英和辞書

翻訳と辞書　辞書検索 [ 開発暫定版 ]

スポンサードリンク

Metamath ：ウィキペディア英語版

Metamath

Metamath is a language for developing strictly formalized mathematical definitions and proofs〔(【引用サイトリンク】 title=What is Metamath? )〕 accompanied by a proof checker for this language and a growing database of thousands of proved theorems covering conventional results in logic, set theory, number theory, group theory, algebra, analysis, and topology, as well as topics in Hilbert spaces and quantum logic.〔(【引用サイトリンク】 author=Megill, Norman )〕
==The Metamath language==
While the large database of proved theorems follows conventional ZFC set theory, the Metamath language is a metalanguage, suitable for developing a wide variety of formal systems.
The set of symbols that can be used for constructing formulas is declared using $c
and $v statements; for example:


$( Declare the constant symbols we will use $)
    $c 0 + = -> ( ) term wff |- $.
$( Declare the metavariables we will use $)
    $v t r s P Q $.

The grammar for formulas is specified using a combination of $f
and $a statements; for example:


$( Specify properties of the metavariables $)
    tt $f term t $.
    tr $f term r $.
    ts $f term s $.
    wp $f wff P $.
    wq $f wff Q $.
$( Define "wff" (part 1) $)
    weq $a wff t = r $.
$( Define "wff" (part 2) $)
    wim $a wff ( P -> Q ) $.

Axioms and rules of inference are specified with $a statements
along with $ for block scoping; for example:


$( State axiom a1 $)
    a1 $a |- ( t = r -> ( t = s -> r = s ) ) $.
$( State axiom a2 $)
    a2 $a |- ( t + 0 ) = t $.
    $

The metamath program can convert statements to more conventional TeX notation;
for example, the modus ponens axiom from set.mm:
:

\vdash \varphi\quad\&\quad \vdash ( \varphi \rightarrow \psi )\quad\Rightarrow\quad \vdash \psi

Using one construct, $a statements, to capture syntactic rules, axiom schemas, and rules of inference provides a level of flexibility similar to higher order logical frameworks without a dependency on a complex type system.
Theorems (and derived rules of inference) are written with $p statements;
for example:


$( Prove a theorem $)
    th1 $p |- t = t $=
  $( Here is its proof: $)
       tt tze tpl tt weq tt tt weq tt a2 tt tze tpl
       tt weq tt tze tpl tt weq tt tt weq wim tt a2
       tt tze tpl tt tt a1 mp mp
     $.

Note the inclusion of the proof in the $p statement. It abbreviates
the following detailed proof:


 1 tt            $f term t
 2 tze           $a term 0
 3 1,2 tpl       $a term ( t + 0 )
 4 3,1 weq       $a wff ( t + 0 ) = t
 5 1,1 weq       $a wff t = t
 6 1 a2          $a |- ( t + 0 ) = t
 7 1,2 tpl       $a term ( t + 0 )
 8 7,1 weq       $a wff ( t + 0 ) = t
 9 1,2 tpl       $a term ( t + 0 )
10 9,1 weq       $a wff ( t + 0 ) = t
11 1,1 weq       $a wff t = t
12 10,11 wim     $a wff ( ( t + 0 ) = t -> t = t )
13 1 a2          $a |- ( t + 0 ) = t
14 1,2 tpl       $a term ( t + 0 )
15 14,1,1 a1     $a |- ( ( t + 0 ) = t -> ( ( t + 0 ) = t -> t = t ) )
16 8,12,13,15 mp  $a |- ( ( t + 0 ) = t -> t = t )
17 4,5,6,16 mp   $a |- t = t

The "essential" form of the proof elides syntactic details, leaving a more conventional presentation:


1 a2             $a |- ( t + 0 ) = t
2 a2             $a |- ( t + 0 ) = t
3 a1             $a |- ( ( t + 0 ) = t -> ( ( t + 0 ) = t -> t = t ) )
4 2,3 mp         $a |- ( ( t + 0 ) = t -> t = t )
5 1,4 mp         $a |- t = t

抄文引用元・出典: フリー百科事典『ウィキペディア（Wikipedia）』
■ウィキペディアで「Metamath」の詳細全文を読む

スポンサードリンク

翻訳と辞書 : 翻訳のためのインターネットリソース