オケージョンとナローイング

terminology _

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

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

occasion 構文論, 意味論

context _ narrows 論理 when 構文論 {
  命題 := 自由変数を含む古典論理の論理式
  命題 := 自由変数を含む古典論理の論理式の自由変数をラムダ束縛したラムダ式
  述語 := 述語記号
  述語 := 自由変数を含む古典論理の論理式
  述語 := 自由変数を含む古典論理の論理式の自由変数をラムダ束縛したラムダ式
}

context _ narrows 論理 when 意味論 {
  命題 := 集合圏の真偽値集合を余域とする射
  命題 := 集合圏の特定対象のn-直積を域として真偽値集合を余域とする射
  述語 := 集合圏の真偽値集合を余域とする射
  述語 := 集合圏の特定対象のn-直積を域として真偽値集合を余域とする射
}
  • 命題@論理 ==> {真偽値集合の要素, 集合圏の真偽値集合を余域とする射, 自由変数を含む古典論理の論理式, 自由変数を含む古典論理の論理式の自由変数をラムダ束縛したラムダ式}
  • 命題@論理#構文論 ==> {自由変数を含む古典論理の論理式, 自由変数を含む古典論理の論理式の自由変数をラムダ束縛したラムダ式}