統一的ボキャブラリーと常識的ボキャブラリー

terminology _

vocabulary 圏と射-統一的 {
  0-圏
  1-圏
  0-圏の0-射
  0-圏の1-射
  1-圏の0-射
  1-圏の1-射
  1-圏の恒等1-射
  1-圏の2-射
}

context 圏と射-常識的 for 圏と射-統一的 {
  集合 := 0-圏
  圏 := 1-圏
  集合の要素 := 0-圏の0-射
  集合の要素の等値性 := 0-圏の1-射
  圏の対象 := 1-圏の0-射
  圏の射 := 1-圏の1-射
  圏の対象の等値性 := 1-圏の恒等1-射
  圏の射の等値性 := 1-圏の2-射
}

vocabulary 論理-正確な表現 {
  述語記号
  真偽値集合の要素
  集合圏の真偽値集合のn-直積を域として真偽値集合を余域とする射
  集合圏の特定対象のn-直積を域として真偽値集合を余域とする射
  集合圏の真偽値集合を余域とする射
  自由変数を含む古典論理の論理式
  自由変数を含む古典論理の論理式の自由変数をラムダ束縛したラムダ式
}

context 論理-曖昧な表現 for 論理-正確な表現 {
  命題 := 真偽値集合の要素
  命題 := 集合圏の真偽値集合を余域とする射
  命題 := 自由変数を含む古典論理の論理式
  命題 := 自由変数を含む古典論理の論理式の自由変数をラムダ束縛したラムダ式
  命題関数 := 集合圏の特定対象のn-直積を域として真偽値集合を余域とする射
  命題関数 := 集合圏の真偽値集合のn-直積を域として真偽値集合を余域とする射
  真理関数 := 集合圏の真偽値集合のn-直積を域として真偽値集合を余域とする射
  述語 := 述語記号
  述語 := 集合圏の真偽値集合を余域とする射
  述語 := 自由変数を含む古典論理の論理式
  述語 := 自由変数を含む古典論理の論理式の自由変数をラムダ束縛したラムダ式
}

context 論理-構文的解釈 for 論理-正確な表現 {
  命題 := 自由変数を含む古典論理の論理式
  命題 := 自由変数を含む古典論理の論理式の自由変数をラムダ束縛したラムダ式
  述語 := 述語記号
  述語 := 自由変数を含む古典論理の論理式
  述語 := 自由変数を含む古典論理の論理式の自由変数をラムダ束縛したラムダ式
}

context 論理-意味的解釈 for 論理-正確な表現 {
  命題 := 集合圏の真偽値集合を余域とする射
  命題 := 集合圏の特定対象のn-直積を域として真偽値集合を余域とする射
  述語 := 集合圏の真偽値集合を余域とする射
  述語 := 集合圏の特定対象のn-直積を域として真偽値集合を余域とする射
}